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  645  jcnd  647  annimdc  932  orandc  934  dn1dc  955  syl2an23an  1294  xordidc  1394  nfimd  1578  exlimd2  1588  elex22  2745  elex2  2746  spcimdv  2814  spcimedv  2816  spcedv  2819  rspcdva  2839  elabd  2875  spsbcd  2967  opth  4222  euotd  4239  ssorduni  4471  tfisi  4571  omsinds  4606  nnpredcl  4607  sotri2  5008  sotri3  5009  unielrel  5138  funmo  5213  fnfvima  5730  fliftfun  5775  fliftval  5779  riota5f  5833  riotass2  5835  oprssdmm  6150  tfrlem5  6293  tfrlemibxssdm  6306  tfrlemibfn  6307  tfrlemiex  6310  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemex  6326  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemex  6339  tfrcllemres  6341  tfrcl  6343  rdgisucinc  6364  frecabex  6377  frecabcl  6378  nntr2  6482  ertr  6528  qliftlem  6591  th3q  6618  resixp  6711  f1dom2g  6734  dom3d  6752  en1  6777  xpdom3m  6812  xpf1o  6822  phplem4dom  6840  phpm  6843  phpelm  6844  findcard  6866  finexdc  6880  fiintim  6906  fisseneq  6909  ssfirab  6911  f1dmvrnfibi  6921  iunfidisj  6923  fidcenumlemrk  6931  dcfi  6958  suplub2ti  6978  supelti  6979  ordiso2  7012  caseinl  7068  caseinr  7069  djudom  7070  difinfsn  7077  difinfinf  7078  ctm  7086  enumct  7092  nnnninfeq  7104  ismkvnex  7131  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  acfun  7184  exmidontriimlem2  7199  exmidontriimlem3  7200  cc2lem  7228  cc3  7230  recexnq  7352  ltbtwnnqq  7377  addnnnq0  7411  mulnnnq0  7412  prarloclemn  7461  prarloc  7465  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  ltexprlemrl  7572  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  addsrpr  7707  mulsrpr  7708  map2psrprg  7767  axpre-suploclemres  7863  lemul12a  8778  lemulge11  8782  sup3exmid  8873  nngt0  8903  nn0ge0  9160  nn0ge2m1nn  9195  zletric  9256  zlelttric  9257  nn0n0n1ge2b  9291  nn0ind-raph  9329  supinfneg  9554  infsupneg  9555  infregelbex  9557  rpge0  9623  fz0fzelfz0  10083  fz0fzdiffz0  10086  ige2m2fzo  10154  elfzodifsumelfzo  10157  elfzom1elp1fzo  10158  exfzdc  10196  qletric  10200  qlelttric  10201  rebtwn2zlemshrink  10210  frecuzrdgtcl  10368  frecuzrdg0  10369  frecuzrdgfunlem  10375  frecuzrdg0t  10378  frecuzrdgsuctlem  10379  frecfzennn  10382  seq3f1olemstep  10457  expcl2lemap  10488  leexp1a  10531  expnbnd  10599  faclbnd  10675  faclbnd6  10678  facavg  10680  fihasheqf1oi  10722  fihashf1rn  10723  fihashss  10751  fiubm  10763  seq3coll  10777  resqrexlemdecn  10976  qabsor  11039  cau3lem  11078  xrmaxiflemab  11210  xrmaxadd  11224  climcn2  11272  sumeq2  11322  sumrbdclem  11340  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumgcl  11349  fsum3  11350  isumss  11354  fsumadd  11369  fsum2dlemstep  11397  fisum0diag2  11410  fsummulc2  11411  modfsummodlemstep  11420  fsumabs  11428  fsumrelem  11434  fsumiun  11440  isumshft  11453  mertenslem2  11499  prodeq2  11520  prodrbdclem  11534  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodmul  11554  fprodconst  11583  fprodap0  11584  fprod2dlemstep  11585  fprodrec  11592  fprodsplit1f  11597  fprodap0f  11599  fprodle  11603  sin02gt0  11726  efieq1re  11734  p1modz1  11756  dvdsleabs2  11806  4dvdseven  11876  gcdmndc  11899  zsupcllemstep  11900  infssuzex  11904  gcdsupex  11912  gcdsupcl  11913  gcdeq0  11932  gcdaddm  11939  rppwr  11983  uzwodc  11992  nnwosdc  11994  algfx  12006  eucalgcvga  12012  lcmmndc  12016  lcmval  12017  lcmcllem  12021  lcmledvds  12024  lcmeq0  12025  qredeq  12050  isprm3  12072  prmdc  12084  rpexp  12107  sqpweven  12129  2sqpwodd  12130  phicl2  12168  phibnd  12171  phiprmpw  12176  fermltl  12188  pythagtriplem4  12222  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem14  12231  pythagtriplem16  12233  pclemdc  12242  pcdvdsb  12273  pc2dvds  12283  difsqpwdvds  12291  pcmpt  12295  pcmptdvds  12297  fldivp1  12300  prmpwdvds  12307  infpnlem1  12311  infpnlem2  12312  1arith  12319  ennnfonelemk  12355  ennnfonelemhom  12370  ennnfonelemrnh  12371  ennnfonelemf1  12373  ctinf  12385  ctiunctlemudc  12392  ctiunctlemf  12393  nninfdclemcl  12403  nninfdclemp1  12405  strslfvd  12457  strslfv2d  12458  strslssd  12462  lidrididd  12636  sgrpidmndm  12656  eltg3  12851  iuncld  12909  cnss2  13021  txcnp  13065  uptx  13068  xblm  13211  metss  13288  fsumcncntop  13350  rescncf  13362  dedekindeulemlu  13393  suplociccex  13397  dedekindicclemlu  13402  dedekindicc  13405  ivthdec  13416  limccnp2lem  13439  dvaddxx  13461  dvmulxx  13462  dvrecap  13471  reeff1olem  13486  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgscllem  13702  lgsval2lem  13705  lgsneg  13719  lgsdir2  13728  lgsdir  13730  lgsdi  13732  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  2sqlem6  13750  sumdc2  13834  pwle2  14031  subctctexmid  14034  nninfsellemeq  14047  exmidsbthrlem  14054