Theorem syl5ibcom 245

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 244	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpcd  249  elrab3t  3690  mob2  3720  rmob  3889  sneqrg  4838  preq1b  4845  prel12g  4863  disjxun  5140  sotric  5621  sotrieq  5622  iss  6052  poirr2  6143  xp11  6194  nordeq  6402  nsuceq0  6466  ordequn  6486  tz6.12cOLD  6932  fnbrfvb  6958  foeqcnvco  7321  f1eqcocnv  7322  dfwe2  7795  releldmdifi  8071  mposn  8129  poxp2  8169  poxp3  8176  poseq  8184  tfrlem15  8433  tz7.44-2  8448  tz7.48-1  8484  tz7.49  8486  oawordexr  8595  oewordi  8630  oeeulem  8640  nna0r  8648  nnawordex  8676  nnaordex  8677  nnaordex2  8678  oaabs  8687  oaabs2  8688  eldifsucnn  8703  ectocld  8825  ecoptocl  8848  mapsnd  8927  eqeng  9027  difsnen  9094  fopwdom  9121  nneneq  9247  frfi  9322  elfiun  9471  ordiso  9557  ordtypelem7  9565  wemaplem2  9588  suc11reg  9660  inf3lem6  9674  noinfep  9701  cantnff  9715  cantnfp1lem2  9720  cantnfp1lem3  9721  cantnflem1  9730  cantnf  9734  ttrcltr  9757  r111  9816  rankc2  9912  tcrank  9925  cardnueq0  10005  fodomfi2  10101  alephinit  10136  dfac9  10178  dfac12k  10189  djuinf  10230  ackbij1  10278  ackbij2  10283  sornom  10318  fin23lem16  10376  fin23lem21  10380  isf32lem2  10395  fin1a2lem6  10446  itunitc  10462  zorn2lem4  10540  wunr1om  10760  tskr1om  10808  recmulnq  11005  ltexnq  11016  distrlem4pr  11067  1re  11262  0re  11264  0cnALT  11497  0cnALT2  11498  mulge0  11782  prodgt0  12115  peano2nn  12279  recnz  12695  zneo  12703  uzn0  12896  xlemul1a  13331  prunioo  13522  flidz  13851  ceilidz  13893  modid2  13939  modmuladdnn0  13957  om2uzrani  13994  uzrdgfni  14000  seqid  14089  seqz  14092  facdiv  14327  facwordi  14329  hashdom  14419  wrdnval  14584  wrdnfi  14587  wrdl1s1  14653  sqrmo  15291  fsumf1o  15760  isumltss  15885  supcvg  15893  dvdsnegb  16312  dvdsexp2im  16365  odd2np1lem  16378  odd2np1  16379  ltoddhalfle  16399  halfleoddlt  16400  opoe  16401  omoe  16402  opeo  16403  omeo  16404  bitsuz  16512  bezoutlem4  16580  gcddiv  16589  gcdzeq  16590  dvdssqim  16592  dvdsexpim  16593  lcmgcdeq  16650  coprmdvds2  16692  rpmul  16697  divgcdcoprmex  16704  cncongr2  16706  dvdsprm  16741  coprm  16749  prmdvdsexp  16753  prmdiv  16823  pythagtriplem19  16872  pc2dvds  16918  pcadd  16928  prmpwdvds  16943  vdwlem11  17030  ramubcl  17057  0ram  17059  posasymb  18366  pleval2  18383  pltval3  18385  plttr  18388  pospo  18391  letsr  18639  intopsn  18668  ismgmid  18679  imasmnd2  18788  isgrpid2  18995  isgrpinv  19012  dfgrp3lem  19057  imasgrp2  19074  orbsta  19332  symgfix2  19435  pmtrfrn  19477  pmtrrn2  19479  odmulg  19575  odmulgeq  19576  gexdvdsi  19602  gexnnod  19607  pgpssslw  19633  sylow2alem1  19636  fislw  19644  lsmss1b  19685  lsmss2b  19687  efgrelexlemb  19769  torsubg  19873  ablfacrplem  20086  pgpfac1lem2  20096  pgpfac1lem3  20098  ablsimpnosubgd  20125  imasrng  20175  imasring  20328  dvdsrcl2  20367  dvdsrtr  20369  dvdsrmul1  20370  irredn0  20424  lspsneq0  21011  lmhmima  21047  lspsolv  21146  xrsdsreclblem  21431  dvdsrzring  21473  prmirredlem  21484  znunit  21583  pjdm2  21732  obselocv  21749  lindfrn  21842  opsrtoslem2  22081  mpfind  22132  psdmul  22171  mpfpf1  22356  pf1mpf  22357  cpmadugsumlemF  22883  baspartn  22962  bastop  22989  iscld3  23073  isopn3  23075  iscldtop  23104  ordtrest2lem  23212  2ndcredom  23459  2ndc1stc  23460  2ndcrest  23463  2ndcdisj  23465  2ndcsep  23468  kgenidm  23556  dfac14  23627  tx2ndc  23660  kqreglem1  23750  rnelfm  23962  fmfnfmlem2  23964  fmfnfmlem4  23966  fmfnfm  23967  flimtopon  23979  fclstopon  24021  xrsmopn  24835  icccmplem2  24846  reconnlem1  24849  iccpnfcnv  24976  cphsqrtcl2  25221  ivthlem3  25489  ivthicc  25494  ovolctb  25526  ioombl  25601  itgabs  25871  itgsplitioo  25874  dvlip  26033  c1liplem1  26036  c1lip1  26037  dvgt0lem1  26042  dvivthlem2  26049  dvne0  26051  lhop1lem  26053  lhop1  26054  lhop2  26055  lhop  26056  dvcvx  26060  itgsubstlem  26090  mdegnn0cl  26111  ig1peu  26215  elply2  26236  plypf1  26252  dgreq0  26306  aannenlem3  26373  abelthlem2  26477  lognegb  26633  eflogeq  26645  efopn  26701  cxpge0  26726  cxplea  26739  cxple2  26740  cxpcn3lem  26791  cxpaddlelem  26795  cxpaddle  26796  cxpeq  26801  asinsinb  26941  acoscosb  26942  atantanb  26968  wilthlem2  27113  sqf11  27183  sqff1o  27226  ppiublem1  27247  lgsdir  27377  lgsne0  27380  lgsquadlem3  27427  2sqblem  27476  dchrisum0flblem1  27553  ostth3  27683  ostth  27684  noseponlem  27710  nodenselem4  27733  nodenselem5  27734  nodenselem7  27736  nodenselem8  27737  nolt02o  27741  nogt01o  27742  nosupbnd2lem1  27761  noetasuplem4  27782  slerec  27865  madebdayim  27927  negsproplem2  28062  negsunif  28088  slemul1ad  28209  precsexlem6  28237  precsexlem7  28238  noseqp1  28298  om2noseqlt  28306  noseqrdgfn  28313  dfnns2  28363  colinearalg  28926  axcontlem5  28984  axcontlem9  28988  uhgrn0  29085  upgrfn  29105  umgrfn  29117  uvtxnbgrvtx  29411  vtxduhgr0nedg  29511  pthdivtx  29748  iswwlksnx  29861  wpthswwlks2on  29982  clwwlkn  30046  clwwlknonwwlknonb  30126  eupth2lem2  30239  eupth2lem3lem6  30253  htthlem  30937  pjpreeq  31418  h1dn0  31572  spansneleqi  31589  rnbra  32127  dfpjop  32202  elpjrn  32210  stm1i  32263  mdbr2  32316  mdsl2i  32342  sumdmdlem  32438  dmdbr6ati  32443  ordtrest2NEWlem  33922  xrge0iifcnv  33933  eulerpartlemb  34371  erdszelem8  35204  cvmlift3lem4  35328  cvmlift3lem5  35329  fmlasucdisj  35405  mrsub0  35522  mrsubccat  35524  mrsubcn  35525  msubrn  35535  msrid  35551  elmthm  35582  dfon2lem9  35793  btwnconn1lem11  36099  broutsideof2  36124  opnbnd  36327  tailfb  36379  bj-ideqg1  37166  fin2so  37615  lindsadd  37621  poimirlem9  37637  poimirlem17  37645  poimirlem26  37654  poimirlem27  37655  poimirlem31  37659  itgabsnc  37697  ftc2nc  37710  sdclem2  37750  subspopn  37760  equivtotbnd  37786  rngosn3  37932  igenval2  38074  isfldidl  38076  relcnveq3  38323  ecex2  38330  iss2  38346  elrelscnveq3  38493  lshpinN  38991  lsatcv0eq  39049  lsatcv1  39050  cvrnbtwn3  39278  cvrnbtwn4  39281  cvrcmp  39285  atnlt  39315  cvlexchb1  39332  2llnne2N  39411  atcvr0eq  39429  lnnat  39430  cvrat4  39446  ps-1  39480  3at  39493  llncmp  39525  llnnlt  39526  llncvrlpln2  39560  llncvrlpln  39561  lplncmp  39565  lplnnlt  39568  lplncvrlvol2  39618  lplncvrlvol  39619  lvolcmp  39620  lvolnltN  39621  dalempnes  39654  dalemqnet  39655  dalem-cly  39674  dalem44  39719  lncmp  39786  cdlemblem  39796  llnexch2N  39873  osumcllem4N  39962  pexmidlem1N  39973  lhp2atnle  40036  cdleme11dN  40265  cdleme20k  40322  cdleme21at  40331  cdleme21ct  40332  cdleme32e  40448  cdleme35f  40457  tendoex  40978  dochexmidlem1  41463  lcfrlem9  41553  mapd1o  41651  mapdindp3  41725  zndvdchrrhm  41973  elre0re  42295  flt0  42652  ismrc  42717  pellexlem1  42845  aomclem4  43074  dfac21  43083  lsmfgcl  43091  lmhmfgima  43101  dfacbasgrp  43125  hbtlem6  43146  fiuneneq  43209  oaabsb  43312  cantnfresb  43342  stoweidlem27  46047  stoweidlem29  46049  fcoresf1  47086  tz6.12c-afv2  47259  dfatbrafv2b  47262  fnbrafv2b  47265  iccpartrn  47422  prmdvdsfmtnof1lem2  47577  mod42tp1mod8  47594  isubgredg  47857  isuspgrim0  47877  grimuhgr  47883  grimcnv  47884  assintopass  48135  rrxsphere  48674