Theorem syl5ibcom 246

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 245	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  biimpcd  250  elrab3t  3612  mob2  3637  rmob  3797  sneqrg  4671  preq1b  4678  prel12g  4695  disjxun  4954  sotric  5381  sotrieq  5382  iss  5776  poirr2  5852  xp11  5900  nordeq  6077  nsuceq0  6138  ordequn  6158  tz6.12c  6555  fnbrfvb  6578  foeqcnvco  6912  f1eqcocnv  6913  dfwe2  7343  releldmdifi  7591  mposn  7645  tfrlem15  7871  tz7.44-2  7886  tz7.48-1  7921  tz7.49  7923  oawordexr  8023  oewordi  8058  oeeulem  8068  nna0r  8076  nnawordex  8104  nnaordex  8105  oaabs  8112  oaabs2  8113  ectocld  8205  ecoptocl  8228  mapsnd  8289  eqeng  8381  difsnen  8436  fopwdom  8462  frfi  8599  elfiun  8730  ordiso  8816  ordtypelem7  8824  wemaplem2  8847  suc11reg  8917  inf3lem6  8931  noinfep  8958  cantnff  8972  cantnfp1lem2  8977  cantnfp1lem3  8978  cantnflem1  8987  cantnf  8991  r111  9039  rankc2  9135  tcrank  9148  cardnueq0  9228  fodomfi2  9321  alephinit  9356  dfac9  9397  dfac12k  9408  djuinf  9449  ackbij1  9495  ackbij2  9500  sornom  9534  fin23lem16  9592  fin23lem21  9596  isf32lem2  9611  fin1a2lem6  9662  itunitc  9678  zorn2lem4  9756  wunr1om  9976  tskr1om  10024  recmulnq  10221  ltexnq  10232  distrlem4pr  10283  1re  10476  0re  10478  0cnALT  10710  0cnALT2  10711  mulge0  10995  prodgt0  11324  peano2nn  11487  recnz  11895  zneo  11903  uzn0  12098  xlemul1a  12520  prunioo  12706  flidz  13018  ceilidz  13058  modid2  13104  modmuladdnn0  13121  om2uzrani  13158  uzrdgfni  13164  seqid  13253  seqz  13256  facdiv  13485  facwordi  13487  hashdom  13576  wrdnval  13730  wrdnfi  13733  wrdl1s1  13800  sqrmo  14433  fsumf1o  14901  isumltss  15024  supcvg  15032  dvdsnegb  15448  odd2np1lem  15510  odd2np1  15511  ltoddhalfle  15531  halfleoddlt  15532  opoe  15533  omoe  15534  opeo  15535  omeo  15536  bitsuz  15644  bezoutlem4  15707  gcddiv  15716  gcdzeq  15719  dvdssqim  15721  lcmgcdeq  15773  coprmdvds2  15815  rpmul  15820  divgcdcoprmex  15827  cncongr2  15829  dvdsprm  15864  coprm  15872  prmdvdsexp  15876  prmdiv  15939  pythagtriplem19  15987  pc2dvds  16032  pcadd  16042  prmpwdvds  16057  vdwlem11  16144  ramubcl  16171  0ram  16173  posasymb  17379  pleval2  17392  pltval3  17394  plttr  17397  pospo  17400  letsr  17654  intopsn  17680  ismgmid  17691  imasmnd2  17754  isgrpid2  17885  isgrpinv  17901  dfgrp3lem  17942  imasgrp2  17959  orbsta  18172  symgfix2  18263  pmtrfrn  18305  pmtrrn2  18307  odmulg  18401  odmulgeq  18402  gexdvdsi  18426  gexnnod  18431  pgpssslw  18457  sylow2alem1  18460  fislw  18468  lsmss1b  18508  lsmss2b  18510  efgrelexlemb  18591  torsubg  18685  ablfacrplem  18892  pgpfac1lem2  18902  pgpfac1lem3  18904  imasring  19047  dvdsrcl2  19078  dvdsrtr  19080  dvdsrmul1  19081  irredn0  19131  lspsneq0  19462  lmhmima  19497  lspsolv  19593  opsrtoslem2  19940  mpfind  19991  mpfpf1  20184  pf1mpf  20185  xrsdsreclblem  20261  dvdsrzring  20300  prmirredlem  20310  znunit  20380  pjdm2  20525  obselocv  20542  lindfrn  20635  cpmadugsumlemF  21156  baspartn  21234  bastop  21261  iscld3  21344  isopn3  21346  iscldtop  21375  ordtrest2lem  21483  2ndcredom  21730  2ndc1stc  21731  2ndcrest  21734  2ndcdisj  21736  2ndcsep  21739  kgenidm  21827  dfac14  21898  tx2ndc  21931  kqreglem1  22021  rnelfm  22233  fmfnfmlem2  22235  fmfnfmlem4  22237  fmfnfm  22238  flimtopon  22250  fclstopon  22292  xrsmopn  23091  icccmplem2  23102  reconnlem1  23105  iccpnfcnv  23219  cphsqrtcl2  23461  ivthlem3  23725  ivthicc  23730  ovolctb  23762  ioombl  23837  itgabs  24106  itgsplitioo  24109  dvlip  24261  c1liplem1  24264  c1lip1  24265  dvgt0lem1  24270  dvivthlem2  24277  dvne0  24279  lhop1lem  24281  lhop1  24282  lhop2  24283  lhop  24284  dvcvx  24288  itgsubstlem  24316  mdegnn0cl  24336  ig1peu  24436  elply2  24457  plypf1  24473  dgreq0  24526  aannenlem3  24590  abelthlem2  24691  lognegb  24842  eflogeq  24854  efopn  24910  cxpge0  24935  cxplea  24948  cxple2  24949  cxpcn3lem  24997  cxpaddlelem  25001  cxpaddle  25002  cxpeq  25007  asinsinb  25144  acoscosb  25145  atantanb  25171  leibpilem1OLD  25188  wilthlem2  25316  sqf11  25386  sqff1o  25429  ppiublem1  25448  lgsdir  25578  lgsne0  25581  lgsquadlem3  25628  2sqblem  25677  dchrisum0flblem1  25754  ostth3  25884  ostth  25885  colinearalg  26367  axcontlem5  26425  axcontlem9  26429  uhgrn0  26523  upgrfn  26543  umgrfn  26555  uvtxnbgrvtx  26846  vtxduhgr0nedg  26945  pthdivtx  27185  iswwlksnx  27293  wpthswwlks2on  27415  clwwlkn  27479  eupth2lem2  27674  eupth2lem3lem6  27688  htthlem  28373  pjpreeq  28854  h1dn0  29008  spansneleqi  29025  rnbra  29563  dfpjop  29638  elpjrn  29646  stm1i  29699  mdbr2  29752  mdsl2i  29778  sumdmdlem  29874  dmdbr6ati  29879  ordtrest2NEWlem  30738  xrge0iifcnv  30749  eulerpartlemb  31199  erdszelem8  32009  cvmlift3lem4  32133  cvmlift3lem5  32134  fmlasucdisj  32207  mrsub0  32316  mrsubccat  32318  mrsubcn  32319  msubrn  32329  msrid  32345  elmthm  32376  dvdspw  32535  dfon2lem9  32589  poseq  32649  noseponlem  32725  nodenselem4  32745  nodenselem5  32746  nodenselem7  32748  nodenselem8  32749  nolt02o  32753  nosupbnd2lem1  32769  noetalem3  32773  slerec  32831  btwnconn1lem11  33112  broutsideof2  33137  opnbnd  33227  tailfb  33279  bj-ismooredr2  33948  fin2so  34356  lindsadd  34362  poimirlem9  34378  poimirlem17  34386  poimirlem26  34395  poimirlem27  34396  poimirlem31  34400  itgabsnc  34438  ftc2nc  34453  sdclem2  34495  subspopn  34505  equivtotbnd  34534  rngosn3  34680  igenval2  34822  isfldidl  34824  relcnveq3  35058  ecex2  35066  iss2  35083  elrelscnveq3  35212  lshpinN  35606  lsatcv0eq  35664  lsatcv1  35665  cvrnbtwn3  35893  cvrnbtwn4  35896  cvrcmp  35900  atnlt  35930  cvlexchb1  35947  2llnne2N  36025  atcvr0eq  36043  lnnat  36044  cvrat4  36060  ps-1  36094  3at  36107  llncmp  36139  llnnlt  36140  llncvrlpln2  36174  llncvrlpln  36175  lplncmp  36179  lplnnlt  36182  lplncvrlvol2  36232  lplncvrlvol  36233  lvolcmp  36234  lvolnltN  36235  dalempnes  36268  dalemqnet  36269  dalem-cly  36288  dalem44  36333  lncmp  36400  cdlemblem  36410  llnexch2N  36487  osumcllem4N  36576  pexmidlem1N  36587  lhp2atnle  36650  cdleme11dN  36879  cdleme20k  36936  cdleme21at  36945  cdleme21ct  36946  cdleme32e  37062  cdleme35f  37071  tendoex  37592  dochexmidlem1  38077  lcfrlem9  38167  mapd1o  38265  mapdindp3  38339  elre0re  38631  dvdsexpim  38653  ismrc  38733  pellexlem1  38862  aomclem4  39093  dfac21  39102  lsmfgcl  39110  lmhmfgima  39120  dfacbasgrp  39144  hbtlem6  39165  fiuneneq  39233  ablsimpnosubgd  40114  stoweidlem27  41808  stoweidlem29  41810  tz6.12c-afv2  42911  dfatbrafv2b  42914  fnbrafv2b  42917  iccpartrn  43026  prmdvdsfmtnof1lem2  43183  mod42tp1mod8  43203  assintopass  43553  rrxsphere  44170