Theorem syl5ibcom 244

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

Ref	Expression
imbitrid.1	⊢ (𝜑 → 𝜓)
imbitrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibcom	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		imbitrid.1	. . 3 ⊢ (𝜑 → 𝜓)
2		imbitrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	imbitrid 243	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  biimpcd  248  elrab3t  3680  mob2  3709  rmob  3881  sneqrg  4837  preq1b  4844  prel12g  4861  disjxun  5141  sotric  5613  sotrieq  5614  iss  6034  poirr2  6125  xp11  6174  nordeq  6383  nsuceq0  6447  ordequn  6467  tz6.12cOLD  6919  fnbrfvb  6945  foeqcnvco  7304  f1eqcocnv  7305  f1eqcocnvOLD  7306  dfwe2  7771  releldmdifi  8044  mposn  8103  poxp2  8143  poxp3  8150  poseq  8158  tfrlem15  8407  tz7.44-2  8422  tz7.48-1  8458  tz7.49  8460  oawordexr  8571  oewordi  8606  oeeulem  8616  nna0r  8624  nnawordex  8652  nnaordex  8653  nnaordex2  8654  oaabs  8663  oaabs2  8664  eldifsucnn  8679  ectocld  8797  ecoptocl  8820  mapsnd  8899  eqeng  9001  difsnen  9072  fopwdom  9099  nneneq  9228  frfi  9307  elfiun  9448  ordiso  9534  ordtypelem7  9542  wemaplem2  9565  suc11reg  9637  inf3lem6  9651  noinfep  9678  cantnff  9692  cantnfp1lem2  9697  cantnfp1lem3  9698  cantnflem1  9707  cantnf  9711  ttrcltr  9734  r111  9793  rankc2  9889  tcrank  9902  cardnueq0  9982  fodomfi2  10078  alephinit  10113  dfac9  10154  dfac12k  10165  djuinf  10206  ackbij1  10256  ackbij2  10261  sornom  10295  fin23lem16  10353  fin23lem21  10357  isf32lem2  10372  fin1a2lem6  10423  itunitc  10439  zorn2lem4  10517  wunr1om  10737  tskr1om  10785  recmulnq  10982  ltexnq  10993  distrlem4pr  11044  1re  11239  0re  11241  0cnALT  11473  0cnALT2  11474  mulge0  11757  prodgt0  12086  peano2nn  12249  recnz  12662  zneo  12670  uzn0  12864  xlemul1a  13294  prunioo  13485  flidz  13802  ceilidz  13844  modid2  13890  modmuladdnn0  13907  om2uzrani  13944  uzrdgfni  13950  seqid  14039  seqz  14042  facdiv  14273  facwordi  14275  hashdom  14365  wrdnval  14522  wrdnfi  14525  wrdl1s1  14591  sqrmo  15225  fsumf1o  15696  isumltss  15821  supcvg  15829  dvdsnegb  16245  dvdsexp2im  16298  odd2np1lem  16311  odd2np1  16312  ltoddhalfle  16332  halfleoddlt  16333  opoe  16334  omoe  16335  opeo  16336  omeo  16337  bitsuz  16443  bezoutlem4  16512  gcddiv  16521  gcdzeq  16522  dvdssqim  16524  lcmgcdeq  16577  coprmdvds2  16619  rpmul  16624  divgcdcoprmex  16631  cncongr2  16633  dvdsprm  16668  coprm  16676  prmdvdsexp  16680  prmdiv  16748  pythagtriplem19  16796  pc2dvds  16842  pcadd  16852  prmpwdvds  16867  vdwlem11  16954  ramubcl  16981  0ram  16983  posasymb  18305  pleval2  18323  pltval3  18325  plttr  18328  pospo  18331  letsr  18579  intopsn  18608  ismgmid  18619  imasmnd2  18725  isgrpid2  18927  isgrpinv  18944  dfgrp3lem  18988  imasgrp2  19005  orbsta  19258  symgfix2  19365  pmtrfrn  19407  pmtrrn2  19409  odmulg  19505  odmulgeq  19506  gexdvdsi  19532  gexnnod  19537  pgpssslw  19563  sylow2alem1  19566  fislw  19574  lsmss1b  19615  lsmss2b  19617  efgrelexlemb  19699  torsubg  19803  ablfacrplem  20016  pgpfac1lem2  20026  pgpfac1lem3  20028  ablsimpnosubgd  20055  imasrng  20111  imasring  20260  dvdsrcl2  20299  dvdsrtr  20301  dvdsrmul1  20302  irredn0  20356  lspsneq0  20890  lmhmima  20926  lspsolv  21025  xrsdsreclblem  21339  dvdsrzring  21381  prmirredlem  21392  znunit  21491  pjdm2  21639  obselocv  21656  lindfrn  21749  opsrtoslem2  21994  mpfind  22047  psdmul  22084  mpfpf1  22264  pf1mpf  22265  cpmadugsumlemF  22772  baspartn  22851  bastop  22878  iscld3  22962  isopn3  22964  iscldtop  22993  ordtrest2lem  23101  2ndcredom  23348  2ndc1stc  23349  2ndcrest  23352  2ndcdisj  23354  2ndcsep  23357  kgenidm  23445  dfac14  23516  tx2ndc  23549  kqreglem1  23639  rnelfm  23851  fmfnfmlem2  23853  fmfnfmlem4  23855  fmfnfm  23856  flimtopon  23868  fclstopon  23910  xrsmopn  24722  icccmplem2  24733  reconnlem1  24736  iccpnfcnv  24863  cphsqrtcl2  25108  ivthlem3  25376  ivthicc  25381  ovolctb  25413  ioombl  25488  itgabs  25758  itgsplitioo  25761  dvlip  25920  c1liplem1  25923  c1lip1  25924  dvgt0lem1  25929  dvivthlem2  25936  dvne0  25938  lhop1lem  25940  lhop1  25941  lhop2  25942  lhop  25943  dvcvx  25947  itgsubstlem  25977  mdegnn0cl  26001  ig1peu  26103  elply2  26124  plypf1  26140  dgreq0  26194  aannenlem3  26259  abelthlem2  26363  lognegb  26518  eflogeq  26530  efopn  26586  cxpge0  26611  cxplea  26624  cxple2  26625  cxpcn3lem  26676  cxpaddlelem  26680  cxpaddle  26681  cxpeq  26686  asinsinb  26823  acoscosb  26824  atantanb  26850  wilthlem2  26995  sqf11  27065  sqff1o  27108  ppiublem1  27129  lgsdir  27259  lgsne0  27262  lgsquadlem3  27309  2sqblem  27358  dchrisum0flblem1  27435  ostth3  27565  ostth  27566  noseponlem  27591  nodenselem4  27614  nodenselem5  27615  nodenselem7  27617  nodenselem8  27618  nolt02o  27622  nogt01o  27623  nosupbnd2lem1  27642  noetasuplem4  27663  slerec  27746  madebdayim  27808  negsproplem2  27935  negsunif  27961  slemul1ad  28076  precsexlem6  28104  precsexlem7  28105  noseqp1  28158  om2noseqlt  28166  noseqrdgfn  28173  colinearalg  28715  axcontlem5  28773  axcontlem9  28777  uhgrn0  28874  upgrfn  28894  umgrfn  28906  uvtxnbgrvtx  29200  vtxduhgr0nedg  29300  pthdivtx  29537  iswwlksnx  29645  wpthswwlks2on  29766  clwwlkn  29830  clwwlknonwwlknonb  29910  eupth2lem2  30023  eupth2lem3lem6  30037  htthlem  30721  pjpreeq  31202  h1dn0  31356  spansneleqi  31373  rnbra  31911  dfpjop  31986  elpjrn  31994  stm1i  32047  mdbr2  32100  mdsl2i  32126  sumdmdlem  32222  dmdbr6ati  32227  ordtrest2NEWlem  33518  xrge0iifcnv  33529  eulerpartlemb  33983  erdszelem8  34803  cvmlift3lem4  34927  cvmlift3lem5  34928  fmlasucdisj  35004  mrsub0  35121  mrsubccat  35123  mrsubcn  35124  msubrn  35134  msrid  35150  elmthm  35181  dfon2lem9  35382  btwnconn1lem11  35688  broutsideof2  35713  opnbnd  35804  tailfb  35856  bj-ideqg1  36638  fin2so  37075  lindsadd  37081  poimirlem9  37097  poimirlem17  37105  poimirlem26  37114  poimirlem27  37115  poimirlem31  37119  itgabsnc  37157  ftc2nc  37170  sdclem2  37210  subspopn  37220  equivtotbnd  37246  rngosn3  37392  igenval2  37534  isfldidl  37536  relcnveq3  37788  ecex2  37795  iss2  37811  elrelscnveq3  37958  lshpinN  38456  lsatcv0eq  38514  lsatcv1  38515  cvrnbtwn3  38743  cvrnbtwn4  38746  cvrcmp  38750  atnlt  38780  cvlexchb1  38797  2llnne2N  38876  atcvr0eq  38894  lnnat  38895  cvrat4  38911  ps-1  38945  3at  38958  llncmp  38990  llnnlt  38991  llncvrlpln2  39025  llncvrlpln  39026  lplncmp  39030  lplnnlt  39033  lplncvrlvol2  39083  lplncvrlvol  39084  lvolcmp  39085  lvolnltN  39086  dalempnes  39119  dalemqnet  39120  dalem-cly  39139  dalem44  39184  lncmp  39251  cdlemblem  39261  llnexch2N  39338  osumcllem4N  39427  pexmidlem1N  39438  lhp2atnle  39501  cdleme11dN  39730  cdleme20k  39787  cdleme21at  39796  cdleme21ct  39797  cdleme32e  39913  cdleme35f  39922  tendoex  40443  dochexmidlem1  40928  lcfrlem9  41018  mapd1o  41116  mapdindp3  41190  elre0re  41827  dvdsexpim  41879  flt0  42052  ismrc  42112  pellexlem1  42240  aomclem4  42472  dfac21  42481  lsmfgcl  42489  lmhmfgima  42499  dfacbasgrp  42523  hbtlem6  42544  fiuneneq  42611  oaabsb  42714  cantnfresb  42744  stoweidlem27  45406  stoweidlem29  45408  fcoresf1  46442  tz6.12c-afv2  46613  dfatbrafv2b  46616  fnbrafv2b  46619  iccpartrn  46761  prmdvdsfmtnof1lem2  46916  mod42tp1mod8  46933  isuspgrim0  47161  grimuhgr  47167  grimcnv  47168  assintopass  47267  rrxsphere  47812

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »