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  3693  mob2  3723  rmob  3898  sneqrg  4843  preq1b  4850  prel12g  4868  disjxun  5145  sotric  5625  sotrieq  5626  iss  6054  poirr2  6146  xp11  6196  nordeq  6404  nsuceq0  6468  ordequn  6488  tz6.12cOLD  6933  fnbrfvb  6959  foeqcnvco  7319  f1eqcocnv  7320  dfwe2  7792  releldmdifi  8068  mposn  8126  poxp2  8166  poxp3  8173  poseq  8181  tfrlem15  8430  tz7.44-2  8445  tz7.48-1  8481  tz7.49  8483  oawordexr  8592  oewordi  8627  oeeulem  8637  nna0r  8645  nnawordex  8673  nnaordex  8674  nnaordex2  8675  oaabs  8684  oaabs2  8685  eldifsucnn  8700  ectocld  8822  ecoptocl  8845  mapsnd  8924  eqeng  9024  difsnen  9091  fopwdom  9118  nneneq  9243  frfi  9318  elfiun  9467  ordiso  9553  ordtypelem7  9561  wemaplem2  9584  suc11reg  9656  inf3lem6  9670  noinfep  9697  cantnff  9711  cantnfp1lem2  9716  cantnfp1lem3  9717  cantnflem1  9726  cantnf  9730  ttrcltr  9753  r111  9812  rankc2  9908  tcrank  9921  cardnueq0  10001  fodomfi2  10097  alephinit  10132  dfac9  10174  dfac12k  10185  djuinf  10226  ackbij1  10274  ackbij2  10279  sornom  10314  fin23lem16  10372  fin23lem21  10376  isf32lem2  10391  fin1a2lem6  10442  itunitc  10458  zorn2lem4  10536  wunr1om  10756  tskr1om  10804  recmulnq  11001  ltexnq  11012  distrlem4pr  11063  1re  11258  0re  11260  0cnALT  11493  0cnALT2  11494  mulge0  11778  prodgt0  12111  peano2nn  12275  recnz  12690  zneo  12698  uzn0  12892  xlemul1a  13326  prunioo  13517  flidz  13846  ceilidz  13888  modid2  13934  modmuladdnn0  13952  om2uzrani  13989  uzrdgfni  13995  seqid  14084  seqz  14087  facdiv  14322  facwordi  14324  hashdom  14414  wrdnval  14579  wrdnfi  14582  wrdl1s1  14648  sqrmo  15286  fsumf1o  15755  isumltss  15880  supcvg  15888  dvdsnegb  16307  dvdsexp2im  16360  odd2np1lem  16373  odd2np1  16374  ltoddhalfle  16394  halfleoddlt  16395  opoe  16396  omoe  16397  opeo  16398  omeo  16399  bitsuz  16507  bezoutlem4  16575  gcddiv  16584  gcdzeq  16585  dvdssqim  16587  dvdsexpim  16588  lcmgcdeq  16645  coprmdvds2  16687  rpmul  16692  divgcdcoprmex  16699  cncongr2  16701  dvdsprm  16736  coprm  16744  prmdvdsexp  16748  prmdiv  16818  pythagtriplem19  16866  pc2dvds  16912  pcadd  16922  prmpwdvds  16937  vdwlem11  17024  ramubcl  17051  0ram  17053  posasymb  18376  pleval2  18394  pltval3  18396  plttr  18399  pospo  18402  letsr  18650  intopsn  18679  ismgmid  18690  imasmnd2  18799  isgrpid2  19006  isgrpinv  19023  dfgrp3lem  19068  imasgrp2  19085  orbsta  19343  symgfix2  19448  pmtrfrn  19490  pmtrrn2  19492  odmulg  19588  odmulgeq  19589  gexdvdsi  19615  gexnnod  19620  pgpssslw  19646  sylow2alem1  19649  fislw  19657  lsmss1b  19698  lsmss2b  19700  efgrelexlemb  19782  torsubg  19886  ablfacrplem  20099  pgpfac1lem2  20109  pgpfac1lem3  20111  ablsimpnosubgd  20138  imasrng  20194  imasring  20343  dvdsrcl2  20382  dvdsrtr  20384  dvdsrmul1  20385  irredn0  20439  lspsneq0  21027  lmhmima  21063  lspsolv  21162  xrsdsreclblem  21447  dvdsrzring  21489  prmirredlem  21500  znunit  21599  pjdm2  21748  obselocv  21765  lindfrn  21858  opsrtoslem2  22097  mpfind  22148  psdmul  22187  mpfpf1  22370  pf1mpf  22371  cpmadugsumlemF  22897  baspartn  22976  bastop  23003  iscld3  23087  isopn3  23089  iscldtop  23118  ordtrest2lem  23226  2ndcredom  23473  2ndc1stc  23474  2ndcrest  23477  2ndcdisj  23479  2ndcsep  23482  kgenidm  23570  dfac14  23641  tx2ndc  23674  kqreglem1  23764  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  fmfnfm  23981  flimtopon  23993  fclstopon  24035  xrsmopn  24847  icccmplem2  24858  reconnlem1  24861  iccpnfcnv  24988  cphsqrtcl2  25233  ivthlem3  25501  ivthicc  25506  ovolctb  25538  ioombl  25613  itgabs  25884  itgsplitioo  25887  dvlip  26046  c1liplem1  26049  c1lip1  26050  dvgt0lem1  26055  dvivthlem2  26062  dvne0  26064  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  dvcvx  26073  itgsubstlem  26103  mdegnn0cl  26124  ig1peu  26228  elply2  26249  plypf1  26265  dgreq0  26319  aannenlem3  26386  abelthlem2  26490  lognegb  26646  eflogeq  26658  efopn  26714  cxpge0  26739  cxplea  26752  cxple2  26753  cxpcn3lem  26804  cxpaddlelem  26808  cxpaddle  26809  cxpeq  26814  asinsinb  26954  acoscosb  26955  atantanb  26981  wilthlem2  27126  sqf11  27196  sqff1o  27239  ppiublem1  27260  lgsdir  27390  lgsne0  27393  lgsquadlem3  27440  2sqblem  27489  dchrisum0flblem1  27566  ostth3  27696  ostth  27697  noseponlem  27723  nodenselem4  27746  nodenselem5  27747  nodenselem7  27749  nodenselem8  27750  nolt02o  27754  nogt01o  27755  nosupbnd2lem1  27774  noetasuplem4  27795  slerec  27878  madebdayim  27940  negsproplem2  28075  negsunif  28101  slemul1ad  28222  precsexlem6  28250  precsexlem7  28251  noseqp1  28311  om2noseqlt  28319  noseqrdgfn  28326  dfnns2  28376  colinearalg  28939  axcontlem5  28997  axcontlem9  29001  uhgrn0  29098  upgrfn  29118  umgrfn  29130  uvtxnbgrvtx  29424  vtxduhgr0nedg  29524  pthdivtx  29761  iswwlksnx  29869  wpthswwlks2on  29990  clwwlkn  30054  clwwlknonwwlknonb  30134  eupth2lem2  30247  eupth2lem3lem6  30261  htthlem  30945  pjpreeq  31426  h1dn0  31580  spansneleqi  31597  rnbra  32135  dfpjop  32210  elpjrn  32218  stm1i  32271  mdbr2  32324  mdsl2i  32350  sumdmdlem  32446  dmdbr6ati  32451  ordtrest2NEWlem  33882  xrge0iifcnv  33893  eulerpartlemb  34349  erdszelem8  35182  cvmlift3lem4  35306  cvmlift3lem5  35307  fmlasucdisj  35383  mrsub0  35500  mrsubccat  35502  mrsubcn  35503  msubrn  35513  msrid  35529  elmthm  35560  dfon2lem9  35772  btwnconn1lem11  36078  broutsideof2  36103  opnbnd  36307  tailfb  36359  bj-ideqg1  37146  fin2so  37593  lindsadd  37599  poimirlem9  37615  poimirlem17  37623  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  itgabsnc  37675  ftc2nc  37688  sdclem2  37728  subspopn  37738  equivtotbnd  37764  rngosn3  37910  igenval2  38052  isfldidl  38054  relcnveq3  38302  ecex2  38309  iss2  38325  elrelscnveq3  38472  lshpinN  38970  lsatcv0eq  39028  lsatcv1  39029  cvrnbtwn3  39257  cvrnbtwn4  39260  cvrcmp  39264  atnlt  39294  cvlexchb1  39311  2llnne2N  39390  atcvr0eq  39408  lnnat  39409  cvrat4  39425  ps-1  39459  3at  39472  llncmp  39504  llnnlt  39505  llncvrlpln2  39539  llncvrlpln  39540  lplncmp  39544  lplnnlt  39547  lplncvrlvol2  39597  lplncvrlvol  39598  lvolcmp  39599  lvolnltN  39600  dalempnes  39633  dalemqnet  39634  dalem-cly  39653  dalem44  39698  lncmp  39765  cdlemblem  39775  llnexch2N  39852  osumcllem4N  39941  pexmidlem1N  39952  lhp2atnle  40015  cdleme11dN  40244  cdleme20k  40301  cdleme21at  40310  cdleme21ct  40311  cdleme32e  40427  cdleme35f  40436  tendoex  40957  dochexmidlem1  41442  lcfrlem9  41532  mapd1o  41630  mapdindp3  41704  zndvdchrrhm  41952  elre0re  42273  flt0  42623  ismrc  42688  pellexlem1  42816  aomclem4  43045  dfac21  43054  lsmfgcl  43062  lmhmfgima  43072  dfacbasgrp  43096  hbtlem6  43117  fiuneneq  43180  oaabsb  43283  cantnfresb  43313  stoweidlem27  45982  stoweidlem29  45984  fcoresf1  47018  tz6.12c-afv2  47191  dfatbrafv2b  47194  fnbrafv2b  47197  iccpartrn  47354  prmdvdsfmtnof1lem2  47509  mod42tp1mod8  47526  isubgredg  47789  isuspgrim0  47809  grimuhgr  47815  grimcnv  47816  assintopass  48057  rrxsphere  48597