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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl3c  63  mpsyl  65  imp  123  2thd  174  jca  301  syl2anc  404  jc  616  annimdc  884  orandc  886  dn1dc  907  syl2an23an  1236  xordidc  1336  nfimd  1523  exlimd2  1532  elex22  2635  elex2  2636  spcimdv  2704  spcimedv  2706  rspcdva  2728  spsbcd  2853  opth  4073  euotd  4090  ssorduni  4317  tfisi  4415  omsinds  4448  nnpredcl  4449  sotri2  4842  sotri3  4843  unielrel  4971  funmo  5043  fnfvima  5543  fliftfun  5589  fliftval  5593  riota5f  5646  riotass2  5648  tfrlem5  6093  tfrlemibxssdm  6106  tfrlemibfn  6107  tfrlemiex  6110  tfr1onlemsucfn  6119  tfr1onlemsucaccv  6120  tfr1onlembxssdm  6122  tfr1onlembfn  6123  tfr1onlemex  6126  tfr1onlemres  6128  tfrcllemsucfn  6132  tfrcllemsucaccv  6133  tfrcllembxssdm  6135  tfrcllembfn  6136  tfrcllemex  6139  tfrcllemres  6141  tfrcl  6143  rdgisucinc  6164  frecabex  6177  frecabcl  6178  ertr  6321  qliftlem  6384  th3q  6411  resixp  6504  f1dom2g  6527  dom3d  6545  en1  6570  xpdom3m  6604  xpf1o  6614  phplem4dom  6632  phpm  6635  phpelm  6636  findcard  6658  finexdc  6672  fiintim  6693  fisseneq  6696  ssfirab  6697  f1dmvrnfibi  6707  iunfidisj  6709  fidcenumlemrk  6717  suplub2ti  6750  supelti  6751  ordiso2  6782  caseinl  6836  djudom  6837  ctm  6845  enumct  6847  exmidfodomrlemr  6889  exmidfodomrlemrALT  6890  recexnq  7010  ltbtwnnqq  7035  addnnnq0  7069  mulnnnq0  7070  prarloclemn  7119  prarloc  7123  distrlem1prl  7202  distrlem1pru  7203  distrlem4prl  7204  distrlem4pru  7205  ltexprlemrl  7230  cauappcvgprlemladdru  7276  cauappcvgprlemladdrl  7277  addsrpr  7352  mulsrpr  7353  lemul12a  8384  lemulge11  8388  nngt0  8508  nn0ge0  8759  nn0ge2m1nn  8794  zletric  8855  zlelttric  8856  nn0n0n1ge2b  8887  nn0ind-raph  8924  supinfneg  9144  infsupneg  9145  rpge0  9207  fz0fzelfz0  9599  fz0fzdiffz0  9602  ige2m2fzo  9670  elfzodifsumelfzo  9673  elfzom1elp1fzo  9674  exfzdc  9712  qletric  9716  qlelttric  9717  rebtwn2zlemshrink  9726  frecuzrdgtcl  9880  frecuzrdg0  9881  frecuzrdgfunlem  9887  frecuzrdg0t  9890  frecuzrdgsuctlem  9891  frecfzennn  9894  seq3f1olemstep  9991  expcl2lemap  10028  leexp1a  10071  expnbnd  10138  faclbnd  10210  faclbnd6  10213  facavg  10215  fihasheqf1oi  10257  fihashf1rn  10258  fihashss  10285  iseqcoll  10308  resqrexlemdecn  10506  qabsor  10569  cau3lem  10608  climcn2  10759  sumeq2  10809  isumrblem  10826  isummolem3  10831  isummolem2a  10832  zisum  10835  fsumgcl  10838  fisum  10839  isumss  10844  fsumadd  10861  isummulc2  10881  fsum2dlemstep  10889  fisum0diag2  10902  fsummulc2  10903  modfsummodlemstep  10912  fsumabs  10920  fsumrelem  10926  fsumiun  10932  isumshft  10945  mertenslem2  10991  sin02gt0  11115  efieq1re  11122  dvdsleabs2  11186  4dvdseven  11256  gcdmndc  11279  zsupcllemstep  11280  infssuzex  11284  gcdsupex  11288  gcdsupcl  11289  gcdeq0  11307  gcdaddm  11314  rppwr  11356  algfx  11373  eucalgcvga  11379  lcmmndc  11383  lcmval  11384  lcmcllem  11388  lcmledvds  11391  lcmeq0  11392  qredeq  11417  isprm3  11439  rpexp  11471  sqpweven  11492  2sqpwodd  11493  phicl2  11529  phibnd  11532  phiprmpw  11537  strslfvd  11596  strslfv2d  11597  strslssd  11601  eltg3  11818  iuncld  11876  rescncf  11910  sumdc2  11972  nninfalllemn  12170  nninfsellemeq  12178  exmidsbthrlem  12184