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  3641  mob2  3669  rmob  3836  sneqrg  4790  preq1b  4797  prel12g  4815  disjxun  5091  sotric  5557  sotrieq  5558  iss  5989  poirr2  6076  xp11  6128  nordeq  6331  nsuceq0  6397  ordequn  6417  fnbrfvb  6878  2f1fvneq  7200  foeqcnvco  7240  f1eqcocnv  7241  dfwe2  7713  releldmdifi  7983  mposn  8039  poxp2  8079  poxp3  8086  poseq  8094  tfrlem15  8317  tz7.44-2  8332  tz7.48-1  8368  tz7.49  8370  oawordexr  8477  oewordi  8512  oeeulem  8522  nna0r  8530  nnawordex  8558  nnaordex  8559  nnaordex2  8560  oaabs  8569  oaabs2  8570  eldifsucnn  8585  elecex  8678  ectocld  8712  ecoptocl  8737  mapsnd  8816  eqeng  8914  difsnen  8978  fopwdom  9004  nneneq  9121  frfi  9175  elfiun  9320  ordiso  9408  ordtypelem7  9416  wemaplem2  9439  suc11reg  9515  inf3lem6  9529  noinfep  9556  cantnff  9570  cantnfp1lem2  9575  cantnfp1lem3  9576  cantnflem1  9585  cantnf  9589  ttrcltr  9612  r111  9674  rankc2  9770  tcrank  9783  cardnueq0  9863  fodomfi2  9957  alephinit  9992  dfac9  10034  dfac12k  10045  djuinf  10086  ackbij1  10134  ackbij2  10139  sornom  10174  fin23lem16  10232  fin23lem21  10236  isf32lem2  10251  fin1a2lem6  10302  itunitc  10318  zorn2lem4  10396  wunr1om  10616  tskr1om  10664  recmulnq  10861  ltexnq  10872  distrlem4pr  10923  1re  11118  0re  11120  0cnALT  11354  0cnALT2  11355  mulge0  11641  prodgt0  11974  peano2nn  12143  recnz  12554  zneo  12562  uzn0  12755  xlemul1a  13193  prunioo  13387  flidz  13720  ceilidz  13762  modid2  13808  modmuladdnn0  13828  om2uzrani  13865  uzrdgfni  13871  seqid  13960  seqz  13963  facdiv  14200  facwordi  14202  hashdom  14292  wrdnval  14458  wrdnfi  14461  wrdl1s1  14528  sqrmo  15164  fsumf1o  15636  isumltss  15761  supcvg  15769  dvdsnegb  16190  dvdsexp2im  16244  odd2np1lem  16257  odd2np1  16258  ltoddhalfle  16278  halfleoddlt  16279  opoe  16280  omoe  16281  opeo  16282  omeo  16283  bitsuz  16391  bezoutlem4  16459  gcddiv  16468  gcdzeq  16469  dvdssqim  16471  dvdsexpim  16472  lcmgcdeq  16529  coprmdvds2  16571  rpmul  16576  divgcdcoprmex  16583  cncongr2  16585  dvdsprm  16620  coprm  16628  prmdvdsexp  16632  prmdiv  16702  pythagtriplem19  16751  pc2dvds  16797  pcadd  16807  prmpwdvds  16822  vdwlem11  16909  ramubcl  16936  0ram  16938  posasymb  18231  pleval2  18247  pltval3  18249  plttr  18252  pospo  18255  letsr  18505  intopsn  18568  ismgmid  18579  imasmnd2  18688  isgrpid2  18895  isgrpinv  18912  dfgrp3lem  18957  imasgrp2  18974  orbsta  19231  symgfix2  19334  pmtrfrn  19376  pmtrrn2  19378  odmulg  19474  odmulgeq  19475  gexdvdsi  19501  gexnnod  19506  pgpssslw  19532  sylow2alem1  19535  fislw  19543  lsmss1b  19584  lsmss2b  19586  efgrelexlemb  19668  torsubg  19772  ablfacrplem  19985  pgpfac1lem2  19995  pgpfac1lem3  19997  ablsimpnosubgd  20024  imasrng  20101  imasring  20254  dvdsrcl2  20290  dvdsrtr  20292  dvdsrmul1  20293  irredn0  20347  lspsneq0  20951  lmhmima  20987  lspsolv  21086  xrsdsreclblem  21355  dvdsrzring  21404  prmirredlem  21415  znunit  21506  pjdm2  21654  obselocv  21671  lindfrn  21764  opsrtoslem2  21997  mpfind  22048  psdmul  22087  mpfpf1  22272  pf1mpf  22273  cpmadugsumlemF  22797  baspartn  22875  bastop  22902  iscld3  22985  isopn3  22987  iscldtop  23016  ordtrest2lem  23124  2ndcredom  23371  2ndc1stc  23372  2ndcrest  23375  2ndcdisj  23377  2ndcsep  23380  kgenidm  23468  dfac14  23539  tx2ndc  23572  kqreglem1  23662  rnelfm  23874  fmfnfmlem2  23876  fmfnfmlem4  23878  fmfnfm  23879  flimtopon  23891  fclstopon  23933  xrsmopn  24734  icccmplem2  24745  reconnlem1  24748  iccpnfcnv  24875  cphsqrtcl2  25119  ivthlem3  25387  ivthicc  25392  ovolctb  25424  ioombl  25499  itgabs  25769  itgsplitioo  25772  dvlip  25931  c1liplem1  25934  c1lip1  25935  dvgt0lem1  25940  dvivthlem2  25947  dvne0  25949  lhop1lem  25951  lhop1  25952  lhop2  25953  lhop  25954  dvcvx  25958  itgsubstlem  25988  mdegnn0cl  26009  ig1peu  26113  elply2  26134  plypf1  26150  dgreq0  26204  aannenlem3  26271  abelthlem2  26375  lognegb  26532  eflogeq  26544  efopn  26600  cxpge0  26625  cxplea  26638  cxple2  26639  cxpcn3lem  26690  cxpaddlelem  26694  cxpaddle  26695  cxpeq  26700  asinsinb  26840  acoscosb  26841  atantanb  26867  wilthlem2  27012  sqf11  27082  sqff1o  27125  ppiublem1  27146  lgsdir  27276  lgsne0  27279  lgsquadlem3  27326  2sqblem  27375  dchrisum0flblem1  27452  ostth3  27582  ostth  27583  noseponlem  27609  nodenselem4  27632  nodenselem5  27633  nodenselem7  27635  nodenselem8  27636  nolt02o  27640  nogt01o  27641  nosupbnd2lem1  27660  noetasuplem4  27681  slerec  27766  madebdayim  27839  negsproplem2  27977  negsunif  28003  slemul1ad  28127  precsexlem6  28156  precsexlem7  28157  noseqp1  28227  om2noseqlt  28235  noseqrdgfn  28242  bdayn0sf1o  28301  dfnns2  28303  colinearalg  28895  axcontlem5  28953  axcontlem9  28957  uhgrn0  29052  upgrfn  29072  umgrfn  29084  uvtxnbgrvtx  29378  vtxduhgr0nedg  29478  pthdivtx  29712  iswwlksnx  29825  wpthswwlks2on  29949  clwwlkn  30013  clwwlknonwwlknonb  30093  eupth2lem2  30206  eupth2lem3lem6  30220  htthlem  30904  pjpreeq  31385  h1dn0  31539  spansneleqi  31556  rnbra  32094  dfpjop  32169  elpjrn  32177  stm1i  32230  mdbr2  32283  mdsl2i  32309  sumdmdlem  32405  dmdbr6ati  32410  ordtrest2NEWlem  33942  xrge0iifcnv  33953  eulerpartlemb  34388  onvf1odlem4  35157  erdszelem8  35249  cvmlift3lem4  35373  cvmlift3lem5  35374  fmlasucdisj  35450  mrsub0  35567  mrsubccat  35569  mrsubcn  35570  msubrn  35580  msrid  35596  elmthm  35627  dfon2lem9  35840  btwnconn1lem11  36148  broutsideof2  36173  opnbnd  36376  tailfb  36428  bj-ideqg1  37215  fin2so  37653  lindsadd  37659  poimirlem9  37675  poimirlem17  37683  poimirlem26  37692  poimirlem27  37693  poimirlem31  37697  itgabsnc  37735  ftc2nc  37748  sdclem2  37788  subspopn  37798  equivtotbnd  37824  rngosn3  37970  igenval2  38112  isfldidl  38114  relcnveq3  38365  iss2  38382  elrelscnveq3  38645  lshpinN  39094  lsatcv0eq  39152  lsatcv1  39153  cvrnbtwn3  39381  cvrnbtwn4  39384  cvrcmp  39388  atnlt  39418  cvlexchb1  39435  2llnne2N  39513  atcvr0eq  39531  lnnat  39532  cvrat4  39548  ps-1  39582  3at  39595  llncmp  39627  llnnlt  39628  llncvrlpln2  39662  llncvrlpln  39663  lplncmp  39667  lplnnlt  39670  lplncvrlvol2  39720  lplncvrlvol  39721  lvolcmp  39722  lvolnltN  39723  dalempnes  39756  dalemqnet  39757  dalem-cly  39776  dalem44  39821  lncmp  39888  cdlemblem  39898  llnexch2N  39975  osumcllem4N  40064  pexmidlem1N  40075  lhp2atnle  40138  cdleme11dN  40367  cdleme20k  40424  cdleme21at  40433  cdleme21ct  40434  cdleme32e  40550  cdleme35f  40559  tendoex  41080  dochexmidlem1  41565  lcfrlem9  41655  mapd1o  41753  mapdindp3  41827  zndvdchrrhm  42071  elre0re  42353  mullt0b2d  42583  flt0  42736  ismrc  42799  pellexlem1  42927  aomclem4  43155  dfac21  43164  lsmfgcl  43172  lmhmfgima  43182  dfacbasgrp  43206  hbtlem6  43227  fiuneneq  43290  oaabsb  43392  cantnfresb  43422  orbitcl  45055  stoweidlem27  46130  stoweidlem29  46132  fcoresf1  47174  tz6.12c-afv2  47347  dfatbrafv2b  47350  fnbrafv2b  47353  iccpartrn  47535  prmdvdsfmtnof1lem2  47690  mod42tp1mod8  47707  isubgredg  47971  grimuhgr  47992  grimcnv  47993  isuspgrim0  47999  assintopass  48319  rrxsphere  48854