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  3647  mob2  3675  rmob  3842  sneqrg  4797  preq1b  4804  prel12g  4822  disjxun  5098  sotric  5570  sotrieq  5571  iss  6002  poirr2  6089  xp11  6141  nordeq  6344  nsuceq0  6410  ordequn  6430  fnbrfvb  6892  2f1fvneq  7216  foeqcnvco  7256  f1eqcocnv  7257  dfwe2  7729  releldmdifi  7999  mposn  8055  poxp2  8095  poxp3  8102  poseq  8110  tfrlem15  8333  tz7.44-2  8348  tz7.48-1  8384  tz7.49  8386  oawordexr  8493  oewordi  8529  oeeulem  8539  nna0r  8547  nnawordex  8575  nnaordex  8576  nnaordex2  8577  oaabs  8586  oaabs2  8587  eldifsucnn  8602  elecex  8696  ectocld  8731  ecoptocl  8756  mapsnd  8836  eqeng  8935  difsnen  8999  fopwdom  9025  nneneq  9142  frfi  9197  elfiun  9345  ordiso  9433  ordtypelem7  9441  wemaplem2  9464  suc11reg  9540  inf3lem6  9554  noinfep  9581  cantnff  9595  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnflem1  9610  cantnf  9614  ttrcltr  9637  r111  9699  rankc2  9795  tcrank  9808  cardnueq0  9888  fodomfi2  9982  alephinit  10017  dfac9  10059  dfac12k  10070  djuinf  10111  ackbij1  10159  ackbij2  10164  sornom  10199  fin23lem16  10257  fin23lem21  10261  isf32lem2  10276  fin1a2lem6  10327  itunitc  10343  zorn2lem4  10421  wunr1om  10642  tskr1om  10690  recmulnq  10887  ltexnq  10898  distrlem4pr  10949  1re  11144  0re  11146  0cnALT  11380  0cnALT2  11381  mulge0  11667  prodgt0  12000  peano2nn  12169  recnz  12579  zneo  12587  uzn0  12780  xlemul1a  13215  prunioo  13409  flidz  13742  ceilidz  13784  modid2  13830  modmuladdnn0  13850  om2uzrani  13887  uzrdgfni  13893  seqid  13982  seqz  13985  facdiv  14222  facwordi  14224  hashdom  14314  wrdnval  14480  wrdnfi  14483  wrdl1s1  14550  sqrmo  15186  fsumf1o  15658  isumltss  15783  supcvg  15791  dvdsnegb  16212  dvdsexp2im  16266  odd2np1lem  16279  odd2np1  16280  ltoddhalfle  16300  halfleoddlt  16301  opoe  16302  omoe  16303  opeo  16304  omeo  16305  bitsuz  16413  bezoutlem4  16481  gcddiv  16490  gcdzeq  16491  dvdssqim  16493  dvdsexpim  16494  lcmgcdeq  16551  coprmdvds2  16593  rpmul  16598  divgcdcoprmex  16605  cncongr2  16607  dvdsprm  16642  coprm  16650  prmdvdsexp  16654  prmdiv  16724  pythagtriplem19  16773  pc2dvds  16819  pcadd  16829  prmpwdvds  16844  vdwlem11  16931  ramubcl  16958  0ram  16960  posasymb  18254  pleval2  18270  pltval3  18272  plttr  18275  pospo  18278  letsr  18528  intopsn  18591  ismgmid  18602  imasmnd2  18711  isgrpid2  18918  isgrpinv  18935  dfgrp3lem  18980  imasgrp2  18997  orbsta  19254  symgfix2  19357  pmtrfrn  19399  pmtrrn2  19401  odmulg  19497  odmulgeq  19498  gexdvdsi  19524  gexnnod  19529  pgpssslw  19555  sylow2alem1  19558  fislw  19566  lsmss1b  19607  lsmss2b  19609  efgrelexlemb  19691  torsubg  19795  ablfacrplem  20008  pgpfac1lem2  20018  pgpfac1lem3  20020  ablsimpnosubgd  20047  imasrng  20124  imasring  20278  dvdsrcl2  20314  dvdsrtr  20316  dvdsrmul1  20317  irredn0  20371  lspsneq0  20975  lmhmima  21011  lspsolv  21110  xrsdsreclblem  21379  dvdsrzring  21428  prmirredlem  21439  znunit  21530  pjdm2  21678  obselocv  21695  lindfrn  21788  opsrtoslem2  22023  mpfind  22082  psdmul  22121  mpfpf1  22307  pf1mpf  22308  cpmadugsumlemF  22832  baspartn  22910  bastop  22937  iscld3  23020  isopn3  23022  iscldtop  23051  ordtrest2lem  23159  2ndcredom  23406  2ndc1stc  23407  2ndcrest  23410  2ndcdisj  23412  2ndcsep  23415  kgenidm  23503  dfac14  23574  tx2ndc  23607  kqreglem1  23697  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  fmfnfm  23914  flimtopon  23926  fclstopon  23968  xrsmopn  24769  icccmplem2  24780  reconnlem1  24783  iccpnfcnv  24910  cphsqrtcl2  25154  ivthlem3  25422  ivthicc  25427  ovolctb  25459  ioombl  25534  itgabs  25804  itgsplitioo  25807  dvlip  25966  c1liplem1  25969  c1lip1  25970  dvgt0lem1  25975  dvivthlem2  25982  dvne0  25984  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  dvcvx  25993  itgsubstlem  26023  mdegnn0cl  26044  ig1peu  26148  elply2  26169  plypf1  26185  dgreq0  26239  aannenlem3  26306  abelthlem2  26410  lognegb  26567  eflogeq  26579  efopn  26635  cxpge0  26660  cxplea  26673  cxple2  26674  cxpcn3lem  26725  cxpaddlelem  26729  cxpaddle  26730  cxpeq  26735  asinsinb  26875  acoscosb  26876  atantanb  26902  wilthlem2  27047  sqf11  27117  sqff1o  27160  ppiublem1  27181  lgsdir  27311  lgsne0  27314  lgsquadlem3  27361  2sqblem  27410  dchrisum0flblem1  27487  ostth3  27617  ostth  27618  noseponlem  27644  nodenselem4  27667  nodenselem5  27668  nodenselem7  27670  nodenselem8  27671  nolt02o  27675  nogt01o  27676  nosupbnd2lem1  27695  noetasuplem4  27716  lesrec  27807  madebdayim  27896  negsproplem2  28037  negsunif  28063  negleft  28066  negright  28067  lemuls1ad  28190  precsexlem6  28220  precsexlem7  28221  noseqp1  28299  om2noseqlt  28307  noseqrdgfn  28314  bdayn0sf1o  28378  dfnns2  28380  bdayfinbndlem1  28475  colinearalg  28995  axcontlem5  29053  axcontlem9  29057  uhgrn0  29152  upgrfn  29172  umgrfn  29184  uvtxnbgrvtx  29478  vtxduhgr0nedg  29578  pthdivtx  29812  iswwlksnx  29925  wpthswwlks2on  30049  clwwlkn  30113  clwwlknonwwlknonb  30193  eupth2lem2  30306  eupth2lem3lem6  30320  htthlem  31004  pjpreeq  31485  h1dn0  31639  spansneleqi  31656  rnbra  32194  dfpjop  32269  elpjrn  32277  stm1i  32330  mdbr2  32383  mdsl2i  32409  sumdmdlem  32505  dmdbr6ati  32510  ordtrest2NEWlem  34099  xrge0iifcnv  34110  eulerpartlemb  34545  onvf1odlem4  35319  erdszelem8  35411  cvmlift3lem4  35535  cvmlift3lem5  35536  fmlasucdisj  35612  mrsub0  35729  mrsubccat  35731  mrsubcn  35732  msubrn  35742  msrid  35758  elmthm  35789  dfon2lem9  36002  btwnconn1lem11  36310  broutsideof2  36335  opnbnd  36538  tailfb  36590  bj-ideqg1  37416  fin2so  37855  lindsadd  37861  poimirlem9  37877  poimirlem17  37885  poimirlem26  37894  poimirlem27  37895  poimirlem31  37899  itgabsnc  37937  ftc2nc  37950  sdclem2  37990  subspopn  38000  equivtotbnd  38026  rngosn3  38172  igenval2  38314  isfldidl  38316  relcnveq3  38575  iss2  38592  elrelscnveq3  38875  lshpinN  39362  lsatcv0eq  39420  lsatcv1  39421  cvrnbtwn3  39649  cvrnbtwn4  39652  cvrcmp  39656  atnlt  39686  cvlexchb1  39703  2llnne2N  39781  atcvr0eq  39799  lnnat  39800  cvrat4  39816  ps-1  39850  3at  39863  llncmp  39895  llnnlt  39896  llncvrlpln2  39930  llncvrlpln  39931  lplncmp  39935  lplnnlt  39938  lplncvrlvol2  39988  lplncvrlvol  39989  lvolcmp  39990  lvolnltN  39991  dalempnes  40024  dalemqnet  40025  dalem-cly  40044  dalem44  40089  lncmp  40156  cdlemblem  40166  llnexch2N  40243  osumcllem4N  40332  pexmidlem1N  40343  lhp2atnle  40406  cdleme11dN  40635  cdleme20k  40692  cdleme21at  40701  cdleme21ct  40702  cdleme32e  40818  cdleme35f  40827  tendoex  41348  dochexmidlem1  41833  lcfrlem9  41923  mapd1o  42021  mapdindp3  42095  zndvdchrrhm  42339  elre0re  42621  mullt0b2d  42851  flt0  42992  ismrc  43055  pellexlem1  43183  aomclem4  43411  dfac21  43420  lsmfgcl  43428  lmhmfgima  43438  dfacbasgrp  43462  hbtlem6  43483  fiuneneq  43546  oaabsb  43648  cantnfresb  43678  orbitcl  45310  stoweidlem27  46382  stoweidlem29  46384  fcoresf1  47426  tz6.12c-afv2  47599  dfatbrafv2b  47602  fnbrafv2b  47605  iccpartrn  47787  prmdvdsfmtnof1lem2  47942  mod42tp1mod8  47959  isubgredg  48223  grimuhgr  48244  grimcnv  48245  isuspgrim0  48251  assintopass  48571  rrxsphere  49105