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  1278  xordidc  1378  nfimd  1565  exlimd2  1575  elex22  2704  elex2  2705  spcimdv  2773  spcimedv  2775  spcedv  2778  rspcdva  2798  elabd  2833  spsbcd  2925  opth  4167  euotd  4184  ssorduni  4411  tfisi  4509  omsinds  4543  nnpredcl  4544  sotri2  4944  sotri3  4945  unielrel  5074  funmo  5146  fnfvima  5660  fliftfun  5705  fliftval  5709  riota5f  5762  riotass2  5764  oprssdmm  6077  tfrlem5  6219  tfrlemibxssdm  6232  tfrlemibfn  6233  tfrlemiex  6236  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemex  6252  tfr1onlemres  6254  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemex  6265  tfrcllemres  6267  tfrcl  6269  rdgisucinc  6290  frecabex  6303  frecabcl  6304  nntr2  6407  ertr  6452  qliftlem  6515  th3q  6542  resixp  6635  f1dom2g  6658  dom3d  6676  en1  6701  xpdom3m  6736  xpf1o  6746  phplem4dom  6764  phpm  6767  phpelm  6768  findcard  6790  finexdc  6804  fiintim  6825  fisseneq  6828  ssfirab  6830  f1dmvrnfibi  6840  iunfidisj  6842  fidcenumlemrk  6850  suplub2ti  6896  supelti  6897  ordiso2  6928  caseinl  6984  caseinr  6985  djudom  6986  difinfsn  6993  difinfinf  6994  ctm  7002  enumct  7008  ismkvnex  7037  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  acfun  7080  cc2lem  7098  cc3  7100  recexnq  7222  ltbtwnnqq  7247  addnnnq0  7281  mulnnnq0  7282  prarloclemn  7331  prarloc  7335  distrlem1prl  7414  distrlem1pru  7415  distrlem4prl  7416  distrlem4pru  7417  ltexprlemrl  7442  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  addsrpr  7577  mulsrpr  7578  map2psrprg  7637  axpre-suploclemres  7733  lemul12a  8644  lemulge11  8648  sup3exmid  8739  nngt0  8769  nn0ge0  9026  nn0ge2m1nn  9061  zletric  9122  zlelttric  9123  nn0n0n1ge2b  9154  nn0ind-raph  9192  supinfneg  9417  infsupneg  9418  rpge0  9483  fz0fzelfz0  9935  fz0fzdiffz0  9938  ige2m2fzo  10006  elfzodifsumelfzo  10009  elfzom1elp1fzo  10010  exfzdc  10048  qletric  10052  qlelttric  10053  rebtwn2zlemshrink  10062  frecuzrdgtcl  10216  frecuzrdg0  10217  frecuzrdgfunlem  10223  frecuzrdg0t  10226  frecuzrdgsuctlem  10227  frecfzennn  10230  seq3f1olemstep  10305  expcl2lemap  10336  leexp1a  10379  expnbnd  10446  faclbnd  10519  faclbnd6  10522  facavg  10524  fihasheqf1oi  10566  fihashf1rn  10567  fihashss  10594  seq3coll  10617  resqrexlemdecn  10816  qabsor  10879  cau3lem  10918  xrmaxiflemab  11048  xrmaxadd  11062  climcn2  11110  sumeq2  11160  sumrbdclem  11178  summodclem3  11181  summodclem2a  11182  zsumdc  11185  fsumgcl  11187  fsum3  11188  isumss  11192  fsumadd  11207  fsum2dlemstep  11235  fisum0diag2  11248  fsummulc2  11249  modfsummodlemstep  11258  fsumabs  11266  fsumrelem  11272  fsumiun  11278  isumshft  11291  mertenslem2  11337  prodeq2  11358  prodrbdclem  11372  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  sin02gt0  11506  efieq1re  11514  dvdsleabs2  11580  4dvdseven  11650  gcdmndc  11673  zsupcllemstep  11674  infssuzex  11678  gcdsupex  11682  gcdsupcl  11683  gcdeq0  11701  gcdaddm  11708  rppwr  11752  algfx  11769  eucalgcvga  11775  lcmmndc  11779  lcmval  11780  lcmcllem  11784  lcmledvds  11787  lcmeq0  11788  qredeq  11813  isprm3  11835  rpexp  11867  sqpweven  11889  2sqpwodd  11890  phicl2  11926  phibnd  11929  phiprmpw  11934  ennnfonelemk  11949  ennnfonelemhom  11964  ennnfonelemrnh  11965  ennnfonelemf1  11967  ctinf  11979  ctiunctlemudc  11986  ctiunctlemf  11987  strslfvd  12039  strslfv2d  12040  strslssd  12044  eltg3  12265  iuncld  12323  cnss2  12435  txcnp  12479  uptx  12482  xblm  12625  metss  12702  fsumcncntop  12764  rescncf  12776  dedekindeulemlu  12807  suplociccex  12811  dedekindicclemlu  12816  dedekindicc  12819  ivthdec  12830  limccnp2lem  12853  dvaddxx  12875  dvmulxx  12876  dvrecap  12885  reeff1olem  12900  sumdc2  13177  pwle2  13366  subctctexmid  13369  nninfalllemn  13377  nninfsellemeq  13385  exmidsbthrlem  13392