Theorem syl5ibcom 247

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimpcd  251  elrab3t  3679  mob2  3706  rmob  3874  sneqrg  4770  preq1b  4777  prel12g  4794  disjxun  5064  sotric  5501  sotrieq  5502  iss  5903  poirr2  5984  xp11  6032  nordeq  6210  nsuceq0  6271  ordequn  6291  tz6.12c  6695  fnbrfvb  6718  foeqcnvco  7056  f1eqcocnv  7057  dfwe2  7496  releldmdifi  7744  mposn  7798  tfrlem15  8028  tz7.44-2  8043  tz7.48-1  8079  tz7.49  8081  oawordexr  8182  oewordi  8217  oeeulem  8227  nna0r  8235  nnawordex  8263  nnaordex  8264  oaabs  8271  oaabs2  8272  ectocld  8364  ecoptocl  8387  mapsnd  8450  eqeng  8543  difsnen  8599  fopwdom  8625  frfi  8763  elfiun  8894  ordiso  8980  ordtypelem7  8988  wemaplem2  9011  suc11reg  9082  inf3lem6  9096  noinfep  9123  cantnff  9137  cantnfp1lem2  9142  cantnfp1lem3  9143  cantnflem1  9152  cantnf  9156  r111  9204  rankc2  9300  tcrank  9313  cardnueq0  9393  fodomfi2  9486  alephinit  9521  dfac9  9562  dfac12k  9573  djuinf  9614  ackbij1  9660  ackbij2  9665  sornom  9699  fin23lem16  9757  fin23lem21  9761  isf32lem2  9776  fin1a2lem6  9827  itunitc  9843  zorn2lem4  9921  wunr1om  10141  tskr1om  10189  recmulnq  10386  ltexnq  10397  distrlem4pr  10448  1re  10641  0re  10643  0cnALT  10874  0cnALT2  10875  mulge0  11158  prodgt0  11487  peano2nn  11650  recnz  12058  zneo  12066  uzn0  12261  xlemul1a  12682  prunioo  12868  flidz  13181  ceilidz  13221  modid2  13267  modmuladdnn0  13284  om2uzrani  13321  uzrdgfni  13327  seqid  13416  seqz  13419  facdiv  13648  facwordi  13650  hashdom  13741  wrdnval  13896  wrdnfi  13899  wrdl1s1  13968  sqrmo  14611  fsumf1o  15080  isumltss  15203  supcvg  15211  dvdsnegb  15627  odd2np1lem  15689  odd2np1  15690  ltoddhalfle  15710  halfleoddlt  15711  opoe  15712  omoe  15713  opeo  15714  omeo  15715  bitsuz  15823  bezoutlem4  15890  gcddiv  15899  gcdzeq  15902  dvdssqim  15904  lcmgcdeq  15956  coprmdvds2  15998  rpmul  16003  divgcdcoprmex  16010  cncongr2  16012  dvdsprm  16047  coprm  16055  prmdvdsexp  16059  prmdiv  16122  pythagtriplem19  16170  pc2dvds  16215  pcadd  16225  prmpwdvds  16240  vdwlem11  16327  ramubcl  16354  0ram  16356  posasymb  17562  pleval2  17575  pltval3  17577  plttr  17580  pospo  17583  letsr  17837  intopsn  17864  ismgmid  17875  imasmnd2  17948  isgrpid2  18140  isgrpinv  18156  dfgrp3lem  18197  imasgrp2  18214  orbsta  18443  symgfix2  18544  pmtrfrn  18586  pmtrrn2  18588  odmulg  18683  odmulgeq  18684  gexdvdsi  18708  gexnnod  18713  pgpssslw  18739  sylow2alem1  18742  fislw  18750  lsmss1b  18792  lsmss2b  18794  efgrelexlemb  18876  torsubg  18974  ablfacrplem  19187  pgpfac1lem2  19197  pgpfac1lem3  19199  ablsimpnosubgd  19226  imasring  19369  dvdsrcl2  19400  dvdsrtr  19402  dvdsrmul1  19403  irredn0  19453  lspsneq0  19784  lmhmima  19819  lspsolv  19915  opsrtoslem2  20265  mpfind  20320  mpfpf1  20514  pf1mpf  20515  xrsdsreclblem  20591  dvdsrzring  20630  prmirredlem  20640  znunit  20710  pjdm2  20855  obselocv  20872  lindfrn  20965  cpmadugsumlemF  21484  baspartn  21562  bastop  21589  iscld3  21672  isopn3  21674  iscldtop  21703  ordtrest2lem  21811  2ndcredom  22058  2ndc1stc  22059  2ndcrest  22062  2ndcdisj  22064  2ndcsep  22067  kgenidm  22155  dfac14  22226  tx2ndc  22259  kqreglem1  22349  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  fmfnfm  22566  flimtopon  22578  fclstopon  22620  xrsmopn  23420  icccmplem2  23431  reconnlem1  23434  iccpnfcnv  23548  cphsqrtcl2  23790  ivthlem3  24054  ivthicc  24059  ovolctb  24091  ioombl  24166  itgabs  24435  itgsplitioo  24438  dvlip  24590  c1liplem1  24593  c1lip1  24594  dvgt0lem1  24599  dvivthlem2  24606  dvne0  24608  lhop1lem  24610  lhop1  24611  lhop2  24612  lhop  24613  dvcvx  24617  itgsubstlem  24645  mdegnn0cl  24665  ig1peu  24765  elply2  24786  plypf1  24802  dgreq0  24855  aannenlem3  24919  abelthlem2  25020  lognegb  25173  eflogeq  25185  efopn  25241  cxpge0  25266  cxplea  25279  cxple2  25280  cxpcn3lem  25328  cxpaddlelem  25332  cxpaddle  25333  cxpeq  25338  asinsinb  25475  acoscosb  25476  atantanb  25502  wilthlem2  25646  sqf11  25716  sqff1o  25759  ppiublem1  25778  lgsdir  25908  lgsne0  25911  lgsquadlem3  25958  2sqblem  26007  dchrisum0flblem1  26084  ostth3  26214  ostth  26215  colinearalg  26696  axcontlem5  26754  axcontlem9  26758  uhgrn0  26852  upgrfn  26872  umgrfn  26884  uvtxnbgrvtx  27175  vtxduhgr0nedg  27274  pthdivtx  27510  iswwlksnx  27618  wpthswwlks2on  27740  clwwlkn  27804  clwwlknonwwlknonb  27885  eupth2lem2  27998  eupth2lem3lem6  28012  htthlem  28694  pjpreeq  29175  h1dn0  29329  spansneleqi  29346  rnbra  29884  dfpjop  29959  elpjrn  29967  stm1i  30020  mdbr2  30073  mdsl2i  30099  sumdmdlem  30195  dmdbr6ati  30200  ordtrest2NEWlem  31165  xrge0iifcnv  31176  eulerpartlemb  31626  erdszelem8  32445  cvmlift3lem4  32569  cvmlift3lem5  32570  fmlasucdisj  32646  mrsub0  32763  mrsubccat  32765  mrsubcn  32766  msubrn  32776  msrid  32792  elmthm  32823  dvdspw  32982  dfon2lem9  33036  poseq  33095  noseponlem  33171  nodenselem4  33191  nodenselem5  33192  nodenselem7  33194  nodenselem8  33195  nolt02o  33199  nosupbnd2lem1  33215  noetalem3  33219  slerec  33277  btwnconn1lem11  33558  broutsideof2  33583  opnbnd  33673  tailfb  33725  bj-ideqg1  34459  fin2so  34894  lindsadd  34900  poimirlem9  34916  poimirlem17  34924  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  itgabsnc  34976  ftc2nc  34991  sdclem2  35032  subspopn  35042  equivtotbnd  35071  rngosn3  35217  igenval2  35359  isfldidl  35361  relcnveq3  35593  ecex2  35600  iss2  35616  elrelscnveq3  35746  lshpinN  36140  lsatcv0eq  36198  lsatcv1  36199  cvrnbtwn3  36427  cvrnbtwn4  36430  cvrcmp  36434  atnlt  36464  cvlexchb1  36481  2llnne2N  36559  atcvr0eq  36577  lnnat  36578  cvrat4  36594  ps-1  36628  3at  36641  llncmp  36673  llnnlt  36674  llncvrlpln2  36708  llncvrlpln  36709  lplncmp  36713  lplnnlt  36716  lplncvrlvol2  36766  lplncvrlvol  36767  lvolcmp  36768  lvolnltN  36769  dalempnes  36802  dalemqnet  36803  dalem-cly  36822  dalem44  36867  lncmp  36934  cdlemblem  36944  llnexch2N  37021  osumcllem4N  37110  pexmidlem1N  37121  lhp2atnle  37184  cdleme11dN  37413  cdleme20k  37470  cdleme21at  37479  cdleme21ct  37480  cdleme32e  37596  cdleme35f  37605  tendoex  38126  dochexmidlem1  38611  lcfrlem9  38701  mapd1o  38799  mapdindp3  38873  elre0re  39203  dvdsexpim  39230  ismrc  39347  pellexlem1  39475  aomclem4  39706  dfac21  39715  lsmfgcl  39723  lmhmfgima  39733  dfacbasgrp  39757  hbtlem6  39778  fiuneneq  39846  stoweidlem27  42361  stoweidlem29  42363  tz6.12c-afv2  43490  dfatbrafv2b  43493  fnbrafv2b  43496  iccpartrn  43639  prmdvdsfmtnof1lem2  43796  mod42tp1mod8  43816  assintopass  44170  rrxsphere  44784