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  3674  mob2  3703  rmob  3876  sneqrg  4832  preq1b  4839  prel12g  4856  disjxun  5136  sotric  5606  sotrieq  5607  iss  6025  poirr2  6115  xp11  6164  nordeq  6373  nsuceq0  6437  ordequn  6457  tz6.12cOLD  6908  fnbrfvb  6934  foeqcnvco  7290  f1eqcocnv  7291  f1eqcocnvOLD  7292  dfwe2  7754  releldmdifi  8024  mposn  8083  poxp2  8123  poxp3  8130  poseq  8138  tfrlem15  8387  tz7.44-2  8402  tz7.48-1  8438  tz7.49  8440  oawordexr  8551  oewordi  8586  oeeulem  8596  nna0r  8604  nnawordex  8632  nnaordex  8633  oaabs  8642  oaabs2  8643  eldifsucnn  8658  ectocld  8773  ecoptocl  8796  mapsnd  8875  eqeng  8977  difsnen  9048  fopwdom  9075  nneneq  9204  frfi  9283  elfiun  9420  ordiso  9506  ordtypelem7  9514  wemaplem2  9537  suc11reg  9609  inf3lem6  9623  noinfep  9650  cantnff  9664  cantnfp1lem2  9669  cantnfp1lem3  9670  cantnflem1  9679  cantnf  9683  ttrcltr  9706  r111  9765  rankc2  9861  tcrank  9874  cardnueq0  9954  fodomfi2  10050  alephinit  10085  dfac9  10126  dfac12k  10137  djuinf  10178  ackbij1  10228  ackbij2  10233  sornom  10267  fin23lem16  10325  fin23lem21  10329  isf32lem2  10344  fin1a2lem6  10395  itunitc  10411  zorn2lem4  10489  wunr1om  10709  tskr1om  10757  recmulnq  10954  ltexnq  10965  distrlem4pr  11016  1re  11210  0re  11212  0cnALT  11444  0cnALT2  11445  mulge0  11728  prodgt0  12057  peano2nn  12220  recnz  12633  zneo  12641  uzn0  12835  xlemul1a  13263  prunioo  13454  flidz  13771  ceilidz  13813  modid2  13859  modmuladdnn0  13876  om2uzrani  13913  uzrdgfni  13919  seqid  14009  seqz  14012  facdiv  14243  facwordi  14245  hashdom  14335  wrdnval  14491  wrdnfi  14494  wrdl1s1  14560  sqrmo  15194  fsumf1o  15665  isumltss  15790  supcvg  15798  dvdsnegb  16213  dvdsexp2im  16266  odd2np1lem  16279  odd2np1  16280  ltoddhalfle  16300  halfleoddlt  16301  opoe  16302  omoe  16303  opeo  16304  omeo  16305  bitsuz  16411  bezoutlem4  16480  gcddiv  16489  gcdzeq  16490  dvdssqim  16492  lcmgcdeq  16545  coprmdvds2  16587  rpmul  16592  divgcdcoprmex  16599  cncongr2  16601  dvdsprm  16636  coprm  16644  prmdvdsexp  16648  prmdiv  16716  pythagtriplem19  16764  pc2dvds  16810  pcadd  16820  prmpwdvds  16835  vdwlem11  16922  ramubcl  16949  0ram  16951  posasymb  18273  pleval2  18291  pltval3  18293  plttr  18296  pospo  18299  letsr  18547  intopsn  18576  ismgmid  18587  imasmnd2  18693  isgrpid2  18895  isgrpinv  18912  dfgrp3lem  18955  imasgrp2  18972  orbsta  19218  symgfix2  19325  pmtrfrn  19367  pmtrrn2  19369  odmulg  19465  odmulgeq  19466  gexdvdsi  19492  gexnnod  19497  pgpssslw  19523  sylow2alem1  19526  fislw  19534  lsmss1b  19575  lsmss2b  19577  efgrelexlemb  19659  torsubg  19763  ablfacrplem  19976  pgpfac1lem2  19986  pgpfac1lem3  19988  ablsimpnosubgd  20015  imasrng  20071  imasring  20218  dvdsrcl2  20257  dvdsrtr  20259  dvdsrmul1  20260  irredn0  20314  lspsneq0  20848  lmhmima  20884  lspsolv  20983  xrsdsreclblem  21274  dvdsrzring  21315  prmirredlem  21326  znunit  21425  pjdm2  21573  obselocv  21590  lindfrn  21683  opsrtoslem2  21926  mpfind  21979  mpfpf1  22191  pf1mpf  22192  cpmadugsumlemF  22699  baspartn  22778  bastop  22805  iscld3  22889  isopn3  22891  iscldtop  22920  ordtrest2lem  23028  2ndcredom  23275  2ndc1stc  23276  2ndcrest  23279  2ndcdisj  23281  2ndcsep  23284  kgenidm  23372  dfac14  23443  tx2ndc  23476  kqreglem1  23566  rnelfm  23778  fmfnfmlem2  23780  fmfnfmlem4  23782  fmfnfm  23783  flimtopon  23795  fclstopon  23837  xrsmopn  24649  icccmplem2  24660  reconnlem1  24663  iccpnfcnv  24790  cphsqrtcl2  25035  ivthlem3  25303  ivthicc  25308  ovolctb  25340  ioombl  25415  itgabs  25685  itgsplitioo  25688  dvlip  25847  c1liplem1  25850  c1lip1  25851  dvgt0lem1  25856  dvivthlem2  25863  dvne0  25865  lhop1lem  25867  lhop1  25868  lhop2  25869  lhop  25870  dvcvx  25874  itgsubstlem  25904  mdegnn0cl  25928  ig1peu  26028  elply2  26049  plypf1  26065  dgreq0  26119  aannenlem3  26183  abelthlem2  26285  lognegb  26439  eflogeq  26451  efopn  26507  cxpge0  26532  cxplea  26545  cxple2  26546  cxpcn3lem  26597  cxpaddlelem  26601  cxpaddle  26602  cxpeq  26607  asinsinb  26744  acoscosb  26745  atantanb  26771  wilthlem2  26916  sqf11  26986  sqff1o  27029  ppiublem1  27050  lgsdir  27180  lgsne0  27183  lgsquadlem3  27230  2sqblem  27279  dchrisum0flblem1  27356  ostth3  27486  ostth  27487  noseponlem  27512  nodenselem4  27535  nodenselem5  27536  nodenselem7  27538  nodenselem8  27539  nolt02o  27543  nogt01o  27544  nosupbnd2lem1  27563  noetasuplem4  27584  slerec  27667  madebdayim  27729  negsproplem2  27856  negsunif  27882  slemul1ad  27997  precsexlem6  28025  precsexlem7  28026  peano2n0s  28086  colinearalg  28603  axcontlem5  28661  axcontlem9  28665  uhgrn0  28762  upgrfn  28782  umgrfn  28794  uvtxnbgrvtx  29085  vtxduhgr0nedg  29184  pthdivtx  29421  iswwlksnx  29529  wpthswwlks2on  29650  clwwlkn  29714  clwwlknonwwlknonb  29794  eupth2lem2  29907  eupth2lem3lem6  29921  htthlem  30605  pjpreeq  31086  h1dn0  31240  spansneleqi  31257  rnbra  31795  dfpjop  31870  elpjrn  31878  stm1i  31931  mdbr2  31984  mdsl2i  32010  sumdmdlem  32106  dmdbr6ati  32111  ordtrest2NEWlem  33357  xrge0iifcnv  33368  eulerpartlemb  33822  erdszelem8  34644  cvmlift3lem4  34768  cvmlift3lem5  34769  fmlasucdisj  34845  mrsub0  34962  mrsubccat  34964  mrsubcn  34965  msubrn  34975  msrid  34991  elmthm  35022  dfon2lem9  35224  btwnconn1lem11  35530  broutsideof2  35555  opnbnd  35666  tailfb  35718  bj-ideqg1  36501  fin2so  36931  lindsadd  36937  poimirlem9  36953  poimirlem17  36961  poimirlem26  36970  poimirlem27  36971  poimirlem31  36975  itgabsnc  37013  ftc2nc  37026  sdclem2  37066  subspopn  37076  equivtotbnd  37102  rngosn3  37248  igenval2  37390  isfldidl  37392  relcnveq3  37646  ecex2  37653  iss2  37669  elrelscnveq3  37817  lshpinN  38315  lsatcv0eq  38373  lsatcv1  38374  cvrnbtwn3  38602  cvrnbtwn4  38605  cvrcmp  38609  atnlt  38639  cvlexchb1  38656  2llnne2N  38735  atcvr0eq  38753  lnnat  38754  cvrat4  38770  ps-1  38804  3at  38817  llncmp  38849  llnnlt  38850  llncvrlpln2  38884  llncvrlpln  38885  lplncmp  38889  lplnnlt  38892  lplncvrlvol2  38942  lplncvrlvol  38943  lvolcmp  38944  lvolnltN  38945  dalempnes  38978  dalemqnet  38979  dalem-cly  38998  dalem44  39043  lncmp  39110  cdlemblem  39120  llnexch2N  39197  osumcllem4N  39286  pexmidlem1N  39297  lhp2atnle  39360  cdleme11dN  39589  cdleme20k  39646  cdleme21at  39655  cdleme21ct  39656  cdleme32e  39772  cdleme35f  39781  tendoex  40302  dochexmidlem1  40787  lcfrlem9  40877  mapd1o  40975  mapdindp3  41049  elre0re  41630  dvdsexpim  41674  flt0  41834  ismrc  41894  pellexlem1  42022  aomclem4  42254  dfac21  42263  lsmfgcl  42271  lmhmfgima  42281  dfacbasgrp  42305  hbtlem6  42326  fiuneneq  42394  oaabsb  42499  cantnfresb  42529  stoweidlem27  45194  stoweidlem29  45196  fcoresf1  46230  tz6.12c-afv2  46401  dfatbrafv2b  46404  fnbrafv2b  46407  iccpartrn  46549  prmdvdsfmtnof1lem2  46704  mod42tp1mod8  46721  assintopass  47043  rrxsphere  47588