Theorem sylc 62

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses

Ref	Expression
sylc.1	|- ( ph -> ps )
sylc.2	|- ( ph -> ch )
sylc.3	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
sylc	|- ( ph -> th )

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 |- ( ph -> ps )
2		sylc.2	. . 3 |- ( ph -> ch )
3		sylc.3	. . 3 |- ( ps -> ( ch -> th ) )
4	1, 2, 3	syl2im 38	. 2 |- ( ph -> ( ph -> th ) )
5	4	pm2.43i 49	1 |- ( ph -> th )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl3c  63  mpsyl  65  imp  124  2thd  175  jca  306  syl2anc  411  jc  654  jcnd  656  annimdc  943  pm4.55dc  944  orandc  945  dn1dc  966  syl2an23an  1333  xordidc  1441  nfimd  1631  exlimd2  1641  elex22  2815  elex2  2816  spcimdv  2887  spcimedv  2889  spcedv  2892  rspcdva  2912  elabd  2948  spsbcd  3041  opth  4323  euotd  4341  ssorduni  4579  tfisi  4679  omsinds  4714  nnpredcl  4715  sotri2  5126  sotri3  5127  unielrel  5256  funmo  5333  fnfvima  5874  fliftfun  5920  fliftval  5924  riota5f  5981  riotass2  5983  fovcld  6109  oprssdmm  6317  tfrlem5  6460  tfrlemibxssdm  6473  tfrlemibfn  6474  tfrlemiex  6477  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemex  6493  tfr1onlemres  6495  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemex  6506  tfrcllemres  6508  tfrcl  6510  rdgisucinc  6531  frecabex  6544  frecabcl  6545  nntr2  6649  ertr  6695  qliftlem  6760  th3q  6787  resixp  6880  f1dom2g  6907  dom3d  6925  domssr  6929  en1  6951  xpdom3m  6993  xpf1o  7005  phplem4dom  7023  phpm  7027  phpelm  7028  findcard  7050  finexdc  7064  fiintim  7093  fisseneq  7096  ssfirab  7098  opabfi  7100  f1dmvrnfibi  7111  iunfidisj  7113  fidcenumlemrk  7121  dcfi  7148  suplub2ti  7168  supelti  7169  ordiso2  7202  caseinl  7258  caseinr  7259  djudom  7260  difinfsn  7267  difinfinf  7268  ctm  7276  enumct  7282  nnnninfeq  7295  ismkvnex  7322  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  acfun  7389  exmidontriimlem2  7404  exmidontriimlem3  7405  exmidapne  7446  cc2lem  7452  cc3  7454  recexnq  7577  ltbtwnnqq  7602  addnnnq0  7636  mulnnnq0  7637  prarloclemn  7686  prarloc  7690  distrlem1prl  7769  distrlem1pru  7770  distrlem4prl  7771  distrlem4pru  7772  ltexprlemrl  7797  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  addsrpr  7932  mulsrpr  7933  map2psrprg  7992  axpre-suploclemres  8088  lemul12a  9009  lemulge11  9013  sup3exmid  9104  nngt0  9135  nn0ge0  9394  nn0ge2m1nn  9429  zletric  9490  zlelttric  9491  nn0n0n1ge2b  9526  nn0ind-raph  9564  supinfneg  9790  infsupneg  9791  infregelbex  9793  rpge0  9862  fz0fzelfz0  10323  fz0fzdiffz0  10326  ige2m2fzo  10404  elfzodifsumelfzo  10407  elfzom1elp1fzo  10408  exfzdc  10446  zsupcllemstep  10449  infssuzex  10453  qletric  10461  qlelttric  10462  rebtwn2zlemshrink  10473  frecuzrdgtcl  10634  frecuzrdg0  10635  frecuzrdgfunlem  10641  frecuzrdg0t  10644  frecuzrdgsuctlem  10645  frecfzennn  10648  seq3f1olemstep  10736  expcl2lemap  10773  leexp1a  10816  expnbnd  10885  faclbnd  10963  faclbnd6  10966  facavg  10968  fihasheqf1oi  11009  fihashf1rn  11010  fihashss  11038  fiubm  11050  seq3coll  11064  wrdsymb0  11104  wrdlenge2n0  11107  ccatsymb  11137  pfxnd  11221  pfxccat1  11234  swrdpfx  11239  pfxpfx  11240  wrd2ind  11255  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  pfxccatpfx1  11268  pfxccatpfx2  11269  swrdccatin1d  11275  pfxccatin12d  11277  resqrexlemdecn  11523  qabsor  11586  cau3lem  11625  xrmaxiflemab  11758  xrmaxadd  11772  climcn2  11820  sumeq2  11870  sumrbdclem  11888  summodclem3  11891  summodclem2a  11892  zsumdc  11895  fsumgcl  11897  fsum3  11898  isumss  11902  fsumadd  11917  fsum2dlemstep  11945  fisum0diag2  11958  fsummulc2  11959  modfsummodlemstep  11968  fsumabs  11976  fsumrelem  11982  fsumiun  11988  isumshft  12001  mertenslem2  12047  prodeq2  12068  prodrbdclem  12082  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodmul  12102  fprodconst  12131  fprodap0  12132  fprod2dlemstep  12133  fprodrec  12140  fprodsplit1f  12145  fprodap0f  12147  fprodle  12151  sin02gt0  12275  efieq1re  12283  p1modz1  12305  dvdsleabs2  12357  4dvdseven  12428  bitsfzo  12466  bitsinv1lem  12472  gcdeq0  12498  rppwr  12549  uzwodc  12558  algfx  12574  eucalgcvga  12580  lcmmndc  12584  lcmeq0  12593  qredeq  12618  isprm3  12640  rpexp  12675  sqpweven  12697  2sqpwodd  12698  phicl2  12736  phibnd  12739  phiprmpw  12744  fermltl  12756  pythagtriplem4  12791  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pythagtriplem16  12802  pcdvdsb  12843  pc2dvds  12853  difsqpwdvds  12861  pcmpt  12866  pcmptdvds  12868  fldivp1  12871  prmpwdvds  12878  infpnlem1  12882  1arith  12890  4sqlem11  12924  ennnfonelemk  12971  ennnfonelemhom  12986  ennnfonelemrnh  12987  ennnfonelemf1  12989  ctinf  13001  ctiunctlemudc  13008  ctiunctlemf  13009  nninfdclemp1  13021  strslfvd  13074  strslfv2d  13075  strslssd  13079  imasival  13339  imasbas  13340  imasplusg  13341  imasaddfnlemg  13347  imasaddvallemg  13348  qusaddvallemg  13366  qusaddflemg  13367  qusaddval  13368  qusaddf  13369  qusmulval  13370  qusmulf  13371  lidrididd  13415  gsumfzval  13424  sgrpidmndm  13453  gsumfzz  13528  qusgrp2  13650  mulgnegnn  13669  eqgen  13764  rinvmod  13846  gsumfzconst  13878  qusrng  13921  srgdilem  13932  ringdilem  13975  qusring2  14029  lssintclm  14348  gsumfzfsumlemm  14551  mplsubgfilemm  14662  eltg3  14731  iuncld  14789  cnss2  14901  txcnp  14945  uptx  14948  xblm  15091  metss  15168  fsumcncntop  15241  rescncf  15255  dedekindeulemlu  15295  suplociccex  15299  dedekindicclemlu  15304  dedekindicc  15307  ivthdec  15318  limccnp2lem  15350  dvaddxx  15377  dvmulxx  15378  dvrecap  15387  reeff1olem  15445  perfectlem2  15674  lgsval  15683  lgsfvalg  15684  lgsfcl2  15685  lgscllem  15686  lgsval2lem  15689  lgsneg  15703  lgsdir2  15712  lgsdir  15714  lgsdi  15716  lgsne0  15717  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem0c  15730  m1lgs  15764  2lgslem1  15770  2lgs  15783  2lgsoddprm  15792  2sqlem6  15799  incistruhgr  15890  upgredg  15942  uhgr2edg  16004  usgriedgdomord  16023  wlkpropg  16037  wlkvtxeledgg  16055  wlk2f  16062  sumdc2  16163  pwle2  16364  subctctexmid  16366  nninfsellemeq  16380  nnnninfex  16388  exmidsbthrlem  16390  cndcap  16427