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  123  2thd  174  jca  304  syl2anc  409  jc  640  jcnd  642  annimdc  922  orandc  924  dn1dc  945  syl2an23an  1281  xordidc  1381  nfimd  1565  exlimd2  1575  elex22  2727  elex2  2728  spcimdv  2796  spcimedv  2798  spcedv  2801  rspcdva  2821  elabd  2857  spsbcd  2949  opth  4197  euotd  4214  ssorduni  4445  tfisi  4545  omsinds  4580  nnpredcl  4581  sotri2  4982  sotri3  4983  unielrel  5112  funmo  5184  fnfvima  5698  fliftfun  5743  fliftval  5747  riota5f  5801  riotass2  5803  oprssdmm  6116  tfrlem5  6258  tfrlemibxssdm  6271  tfrlemibfn  6272  tfrlemiex  6275  tfr1onlemsucfn  6284  tfr1onlemsucaccv  6285  tfr1onlembxssdm  6287  tfr1onlembfn  6288  tfr1onlemex  6291  tfr1onlemres  6293  tfrcllemsucfn  6297  tfrcllemsucaccv  6298  tfrcllembxssdm  6300  tfrcllembfn  6301  tfrcllemex  6304  tfrcllemres  6306  tfrcl  6308  rdgisucinc  6329  frecabex  6342  frecabcl  6343  nntr2  6447  ertr  6492  qliftlem  6555  th3q  6582  resixp  6675  f1dom2g  6698  dom3d  6716  en1  6741  xpdom3m  6776  xpf1o  6786  phplem4dom  6804  phpm  6807  phpelm  6808  findcard  6830  finexdc  6844  fiintim  6870  fisseneq  6873  ssfirab  6875  f1dmvrnfibi  6885  iunfidisj  6887  fidcenumlemrk  6895  suplub2ti  6941  supelti  6942  ordiso2  6973  caseinl  7029  caseinr  7030  djudom  7031  difinfsn  7038  difinfinf  7039  ctm  7047  enumct  7053  nnnninfeq  7065  ismkvnex  7092  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  acfun  7136  exmidontriimlem2  7151  exmidontriimlem3  7152  cc2lem  7180  cc3  7182  recexnq  7304  ltbtwnnqq  7329  addnnnq0  7363  mulnnnq0  7364  prarloclemn  7413  prarloc  7417  distrlem1prl  7496  distrlem1pru  7497  distrlem4prl  7498  distrlem4pru  7499  ltexprlemrl  7524  cauappcvgprlemladdru  7570  cauappcvgprlemladdrl  7571  addsrpr  7659  mulsrpr  7660  map2psrprg  7719  axpre-suploclemres  7815  lemul12a  8727  lemulge11  8731  sup3exmid  8822  nngt0  8852  nn0ge0  9109  nn0ge2m1nn  9144  zletric  9205  zlelttric  9206  nn0n0n1ge2b  9237  nn0ind-raph  9275  supinfneg  9500  infsupneg  9501  rpge0  9566  fz0fzelfz0  10019  fz0fzdiffz0  10022  ige2m2fzo  10090  elfzodifsumelfzo  10093  elfzom1elp1fzo  10094  exfzdc  10132  qletric  10136  qlelttric  10137  rebtwn2zlemshrink  10146  frecuzrdgtcl  10304  frecuzrdg0  10305  frecuzrdgfunlem  10311  frecuzrdg0t  10314  frecuzrdgsuctlem  10315  frecfzennn  10318  seq3f1olemstep  10393  expcl2lemap  10424  leexp1a  10467  expnbnd  10534  faclbnd  10608  faclbnd6  10611  facavg  10613  fihasheqf1oi  10655  fihashf1rn  10656  fihashss  10683  seq3coll  10706  resqrexlemdecn  10905  qabsor  10968  cau3lem  11007  xrmaxiflemab  11137  xrmaxadd  11151  climcn2  11199  sumeq2  11249  sumrbdclem  11267  summodclem3  11270  summodclem2a  11271  zsumdc  11274  fsumgcl  11276  fsum3  11277  isumss  11281  fsumadd  11296  fsum2dlemstep  11324  fisum0diag2  11337  fsummulc2  11338  modfsummodlemstep  11347  fsumabs  11355  fsumrelem  11361  fsumiun  11367  isumshft  11380  mertenslem2  11426  prodeq2  11447  prodrbdclem  11461  prodmodclem3  11465  prodmodclem2a  11466  zproddc  11469  fprodseq  11473  fprodmul  11481  fprodconst  11510  fprodap0  11511  fprod2dlemstep  11512  fprodrec  11519  fprodsplit1f  11524  fprodap0f  11526  fprodle  11530  sin02gt0  11653  efieq1re  11661  p1modz1  11683  dvdsleabs2  11730  4dvdseven  11800  gcdmndc  11823  zsupcllemstep  11824  infssuzex  11828  gcdsupex  11832  gcdsupcl  11833  gcdeq0  11852  gcdaddm  11859  rppwr  11903  algfx  11920  eucalgcvga  11926  lcmmndc  11930  lcmval  11931  lcmcllem  11935  lcmledvds  11938  lcmeq0  11939  qredeq  11964  isprm3  11986  rpexp  12018  sqpweven  12040  2sqpwodd  12041  phicl2  12077  phibnd  12080  phiprmpw  12085  fermltl  12097  ennnfonelemk  12112  ennnfonelemhom  12127  ennnfonelemrnh  12128  ennnfonelemf1  12130  ctinf  12142  ctiunctlemudc  12149  ctiunctlemf  12150  strslfvd  12202  strslfv2d  12203  strslssd  12207  eltg3  12428  iuncld  12486  cnss2  12598  txcnp  12642  uptx  12645  xblm  12788  metss  12865  fsumcncntop  12927  rescncf  12939  dedekindeulemlu  12970  suplociccex  12974  dedekindicclemlu  12979  dedekindicc  12982  ivthdec  12993  limccnp2lem  13016  dvaddxx  13038  dvmulxx  13039  dvrecap  13048  reeff1olem  13063  sumdc2  13344  pwle2  13541  subctctexmid  13544  nninfsellemeq  13557  exmidsbthrlem  13564