Theorem syl5ibcom 248

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

Ref	Expression
syl5ib.1	⊢ (𝜑 → 𝜓)
syl5ib.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibcom	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5ib.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5ib 247	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimpcd  252  elrab3t  3594  mob2  3621  rmob  3793  sneqrg  4740  preq1b  4747  prel12g  4764  disjxun  5041  sotric  5485  sotrieq  5486  iss  5892  poirr2  5978  xp11  6027  nordeq  6221  nsuceq0  6282  ordequn  6302  tz6.12c  6731  fnbrfvb  6754  foeqcnvco  7099  f1eqcocnv  7100  f1eqcocnvOLD  7101  dfwe2  7548  releldmdifi  7805  mposn  7860  tfrlem15  8117  tz7.44-2  8132  tz7.48-1  8168  tz7.49  8170  oawordexr  8273  oewordi  8308  oeeulem  8318  nna0r  8326  nnawordex  8354  nnaordex  8355  oaabs  8362  oaabs2  8363  ectocld  8455  ecoptocl  8478  mapsnd  8556  eqeng  8651  difsnen  8716  fopwdom  8742  frfi  8905  elfiun  9035  ordiso  9121  ordtypelem7  9129  wemaplem2  9152  suc11reg  9223  inf3lem6  9237  noinfep  9264  cantnff  9278  cantnfp1lem2  9283  cantnfp1lem3  9284  cantnflem1  9293  cantnf  9297  r111  9374  rankc2  9470  tcrank  9483  cardnueq0  9563  fodomfi2  9657  alephinit  9692  dfac9  9733  dfac12k  9744  djuinf  9785  ackbij1  9835  ackbij2  9840  sornom  9874  fin23lem16  9932  fin23lem21  9936  isf32lem2  9951  fin1a2lem6  10002  itunitc  10018  zorn2lem4  10096  wunr1om  10316  tskr1om  10364  recmulnq  10561  ltexnq  10572  distrlem4pr  10623  1re  10816  0re  10818  0cnALT  11049  0cnALT2  11050  mulge0  11333  prodgt0  11662  peano2nn  11825  recnz  12235  zneo  12243  uzn0  12438  xlemul1a  12861  prunioo  13052  flidz  13368  ceilidz  13408  modid2  13454  modmuladdnn0  13471  om2uzrani  13508  uzrdgfni  13514  seqid  13604  seqz  13607  facdiv  13836  facwordi  13838  hashdom  13929  wrdnval  14083  wrdnfi  14086  wrdl1s1  14154  sqrmo  14798  fsumf1o  15270  isumltss  15393  supcvg  15401  dvdsnegb  15816  dvdsexp2im  15869  odd2np1lem  15882  odd2np1  15883  ltoddhalfle  15903  halfleoddlt  15904  opoe  15905  omoe  15906  opeo  15907  omeo  15908  bitsuz  16014  bezoutlem4  16083  gcddiv  16092  gcdzeq  16095  dvdssqim  16097  lcmgcdeq  16150  coprmdvds2  16192  rpmul  16197  divgcdcoprmex  16204  cncongr2  16206  dvdsprm  16241  coprm  16249  prmdvdsexp  16253  prmdiv  16319  pythagtriplem19  16367  pc2dvds  16413  pcadd  16423  prmpwdvds  16438  vdwlem11  16525  ramubcl  16552  0ram  16554  posasymb  17798  pleval2  17815  pltval3  17817  plttr  17820  pospo  17823  letsr  18071  intopsn  18098  ismgmid  18109  imasmnd2  18182  isgrpid2  18376  isgrpinv  18392  dfgrp3lem  18433  imasgrp2  18450  orbsta  18679  symgfix2  18780  pmtrfrn  18822  pmtrrn2  18824  odmulg  18919  odmulgeq  18920  gexdvdsi  18944  gexnnod  18949  pgpssslw  18975  sylow2alem1  18978  fislw  18986  lsmss1b  19028  lsmss2b  19030  efgrelexlemb  19112  torsubg  19211  ablfacrplem  19424  pgpfac1lem2  19434  pgpfac1lem3  19436  ablsimpnosubgd  19463  imasring  19609  dvdsrcl2  19640  dvdsrtr  19642  dvdsrmul1  19643  irredn0  19693  lspsneq0  20021  lmhmima  20056  lspsolv  20152  xrsdsreclblem  20381  dvdsrzring  20420  prmirredlem  20431  znunit  20500  pjdm2  20645  obselocv  20662  lindfrn  20755  opsrtoslem2  20985  mpfind  21039  mpfpf1  21239  pf1mpf  21240  cpmadugsumlemF  21745  baspartn  21823  bastop  21850  iscld3  21933  isopn3  21935  iscldtop  21964  ordtrest2lem  22072  2ndcredom  22319  2ndc1stc  22320  2ndcrest  22323  2ndcdisj  22325  2ndcsep  22328  kgenidm  22416  dfac14  22487  tx2ndc  22520  kqreglem1  22610  rnelfm  22822  fmfnfmlem2  22824  fmfnfmlem4  22826  fmfnfm  22827  flimtopon  22839  fclstopon  22881  xrsmopn  23681  icccmplem2  23692  reconnlem1  23695  iccpnfcnv  23813  cphsqrtcl2  24055  ivthlem3  24322  ivthicc  24327  ovolctb  24359  ioombl  24434  itgabs  24704  itgsplitioo  24707  dvlip  24862  c1liplem1  24865  c1lip1  24866  dvgt0lem1  24871  dvivthlem2  24878  dvne0  24880  lhop1lem  24882  lhop1  24883  lhop2  24884  lhop  24885  dvcvx  24889  itgsubstlem  24917  mdegnn0cl  24941  ig1peu  25041  elply2  25062  plypf1  25078  dgreq0  25131  aannenlem3  25195  abelthlem2  25296  lognegb  25450  eflogeq  25462  efopn  25518  cxpge0  25543  cxplea  25556  cxple2  25557  cxpcn3lem  25605  cxpaddlelem  25609  cxpaddle  25610  cxpeq  25615  asinsinb  25752  acoscosb  25753  atantanb  25779  wilthlem2  25923  sqf11  25993  sqff1o  26036  ppiublem1  26055  lgsdir  26185  lgsne0  26188  lgsquadlem3  26235  2sqblem  26284  dchrisum0flblem1  26361  ostth3  26491  ostth  26492  colinearalg  26973  axcontlem5  27031  axcontlem9  27035  uhgrn0  27130  upgrfn  27150  umgrfn  27162  uvtxnbgrvtx  27453  vtxduhgr0nedg  27552  pthdivtx  27788  iswwlksnx  27896  wpthswwlks2on  28017  clwwlkn  28081  clwwlknonwwlknonb  28161  eupth2lem2  28274  eupth2lem3lem6  28288  htthlem  28970  pjpreeq  29451  h1dn0  29605  spansneleqi  29622  rnbra  30160  dfpjop  30235  elpjrn  30243  stm1i  30296  mdbr2  30349  mdsl2i  30375  sumdmdlem  30471  dmdbr6ati  30476  ordtrest2NEWlem  31558  xrge0iifcnv  31569  eulerpartlemb  32019  erdszelem8  32845  cvmlift3lem4  32969  cvmlift3lem5  32970  fmlasucdisj  33046  mrsub0  33163  mrsubccat  33165  mrsubcn  33166  msubrn  33176  msrid  33192  elmthm  33223  dfon2lem9  33455  poxp2  33478  poxp3  33484  poseq  33490  noseponlem  33561  nodenselem4  33584  nodenselem5  33585  nodenselem7  33587  nodenselem8  33588  nolt02o  33592  nogt01o  33593  nosupbnd2lem1  33612  noetasuplem4  33633  slerec  33707  madebdayim  33764  btwnconn1lem11  34093  broutsideof2  34118  opnbnd  34208  tailfb  34260  bj-ideqg1  35027  fin2so  35458  lindsadd  35464  poimirlem9  35480  poimirlem17  35488  poimirlem26  35497  poimirlem27  35498  poimirlem31  35502  itgabsnc  35540  ftc2nc  35553  sdclem2  35594  subspopn  35604  equivtotbnd  35630  rngosn3  35776  igenval2  35918  isfldidl  35920  relcnveq3  36150  ecex2  36157  iss2  36173  elrelscnveq3  36303  lshpinN  36697  lsatcv0eq  36755  lsatcv1  36756  cvrnbtwn3  36984  cvrnbtwn4  36987  cvrcmp  36991  atnlt  37021  cvlexchb1  37038  2llnne2N  37116  atcvr0eq  37134  lnnat  37135  cvrat4  37151  ps-1  37185  3at  37198  llncmp  37230  llnnlt  37231  llncvrlpln2  37265  llncvrlpln  37266  lplncmp  37270  lplnnlt  37273  lplncvrlvol2  37323  lplncvrlvol  37324  lvolcmp  37325  lvolnltN  37326  dalempnes  37359  dalemqnet  37360  dalem-cly  37379  dalem44  37424  lncmp  37491  cdlemblem  37501  llnexch2N  37578  osumcllem4N  37667  pexmidlem1N  37678  lhp2atnle  37741  cdleme11dN  37970  cdleme20k  38027  cdleme21at  38036  cdleme21ct  38037  cdleme32e  38153  cdleme35f  38162  tendoex  38683  dochexmidlem1  39168  lcfrlem9  39258  mapd1o  39356  mapdindp3  39430  elre0re  39950  dvdsexpim  39988  flt0  40129  ismrc  40178  pellexlem1  40306  aomclem4  40537  dfac21  40546  lsmfgcl  40554  lmhmfgima  40564  dfacbasgrp  40588  hbtlem6  40609  fiuneneq  40677  stoweidlem27  43197  stoweidlem29  43199  fcoresf1  44189  tz6.12c-afv2  44360  dfatbrafv2b  44363  fnbrafv2b  44366  iccpartrn  44509  prmdvdsfmtnof1lem2  44664  mod42tp1mod8  44681  assintopass  45035  rrxsphere  45721