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  927  orandc  929  dn1dc  950  syl2an23an  1289  xordidc  1389  nfimd  1573  exlimd2  1583  elex22  2740  elex2  2741  spcimdv  2809  spcimedv  2811  spcedv  2814  rspcdva  2834  elabd  2870  spsbcd  2962  opth  4214  euotd  4231  ssorduni  4463  tfisi  4563  omsinds  4598  nnpredcl  4599  sotri2  5000  sotri3  5001  unielrel  5130  funmo  5202  fnfvima  5718  fliftfun  5763  fliftval  5767  riota5f  5821  riotass2  5823  oprssdmm  6136  tfrlem5  6278  tfrlemibxssdm  6291  tfrlemibfn  6292  tfrlemiex  6295  tfr1onlemsucfn  6304  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemex  6311  tfr1onlemres  6313  tfrcllemsucfn  6317  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemex  6324  tfrcllemres  6326  tfrcl  6328  rdgisucinc  6349  frecabex  6362  frecabcl  6363  nntr2  6467  ertr  6512  qliftlem  6575  th3q  6602  resixp  6695  f1dom2g  6718  dom3d  6736  en1  6761  xpdom3m  6796  xpf1o  6806  phplem4dom  6824  phpm  6827  phpelm  6828  findcard  6850  finexdc  6864  fiintim  6890  fisseneq  6893  ssfirab  6895  f1dmvrnfibi  6905  iunfidisj  6907  fidcenumlemrk  6915  dcfi  6942  suplub2ti  6962  supelti  6963  ordiso2  6996  caseinl  7052  caseinr  7053  djudom  7054  difinfsn  7061  difinfinf  7062  ctm  7070  enumct  7076  nnnninfeq  7088  ismkvnex  7115  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  acfun  7159  exmidontriimlem2  7174  exmidontriimlem3  7175  cc2lem  7203  cc3  7205  recexnq  7327  ltbtwnnqq  7352  addnnnq0  7386  mulnnnq0  7387  prarloclemn  7436  prarloc  7440  distrlem1prl  7519  distrlem1pru  7520  distrlem4prl  7521  distrlem4pru  7522  ltexprlemrl  7547  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  addsrpr  7682  mulsrpr  7683  map2psrprg  7742  axpre-suploclemres  7838  lemul12a  8753  lemulge11  8757  sup3exmid  8848  nngt0  8878  nn0ge0  9135  nn0ge2m1nn  9170  zletric  9231  zlelttric  9232  nn0n0n1ge2b  9266  nn0ind-raph  9304  supinfneg  9529  infsupneg  9530  infregelbex  9532  rpge0  9598  fz0fzelfz0  10058  fz0fzdiffz0  10061  ige2m2fzo  10129  elfzodifsumelfzo  10132  elfzom1elp1fzo  10133  exfzdc  10171  qletric  10175  qlelttric  10176  rebtwn2zlemshrink  10185  frecuzrdgtcl  10343  frecuzrdg0  10344  frecuzrdgfunlem  10350  frecuzrdg0t  10353  frecuzrdgsuctlem  10354  frecfzennn  10357  seq3f1olemstep  10432  expcl2lemap  10463  leexp1a  10506  expnbnd  10574  faclbnd  10650  faclbnd6  10653  facavg  10655  fihasheqf1oi  10697  fihashf1rn  10698  fihashss  10725  fiubm  10737  seq3coll  10751  resqrexlemdecn  10950  qabsor  11013  cau3lem  11052  xrmaxiflemab  11184  xrmaxadd  11198  climcn2  11246  sumeq2  11296  sumrbdclem  11314  summodclem3  11317  summodclem2a  11318  zsumdc  11321  fsumgcl  11323  fsum3  11324  isumss  11328  fsumadd  11343  fsum2dlemstep  11371  fisum0diag2  11384  fsummulc2  11385  modfsummodlemstep  11394  fsumabs  11402  fsumrelem  11408  fsumiun  11414  isumshft  11427  mertenslem2  11473  prodeq2  11494  prodrbdclem  11508  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodseq  11520  fprodmul  11528  fprodconst  11557  fprodap0  11558  fprod2dlemstep  11559  fprodrec  11566  fprodsplit1f  11571  fprodap0f  11573  fprodle  11577  sin02gt0  11700  efieq1re  11708  p1modz1  11730  dvdsleabs2  11780  4dvdseven  11850  gcdmndc  11873  zsupcllemstep  11874  infssuzex  11878  gcdsupex  11886  gcdsupcl  11887  gcdeq0  11906  gcdaddm  11913  rppwr  11957  uzwodc  11966  nnwosdc  11968  algfx  11980  eucalgcvga  11986  lcmmndc  11990  lcmval  11991  lcmcllem  11995  lcmledvds  11998  lcmeq0  11999  qredeq  12024  isprm3  12046  prmdc  12058  rpexp  12081  sqpweven  12103  2sqpwodd  12104  phicl2  12142  phibnd  12145  phiprmpw  12150  fermltl  12162  pythagtriplem4  12196  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem13  12204  pythagtriplem14  12205  pythagtriplem16  12207  pclemdc  12216  pcdvdsb  12247  pc2dvds  12257  difsqpwdvds  12265  pcmpt  12269  pcmptdvds  12271  fldivp1  12274  prmpwdvds  12281  infpnlem1  12285  infpnlem2  12286  1arith  12293  ennnfonelemk  12329  ennnfonelemhom  12344  ennnfonelemrnh  12345  ennnfonelemf1  12347  ctinf  12359  ctiunctlemudc  12366  ctiunctlemf  12367  nninfdclemcl  12377  nninfdclemp1  12379  strslfvd  12431  strslfv2d  12432  strslssd  12436  eltg3  12657  iuncld  12715  cnss2  12827  txcnp  12871  uptx  12874  xblm  13017  metss  13094  fsumcncntop  13156  rescncf  13168  dedekindeulemlu  13199  suplociccex  13203  dedekindicclemlu  13208  dedekindicc  13211  ivthdec  13222  limccnp2lem  13245  dvaddxx  13267  dvmulxx  13268  dvrecap  13277  reeff1olem  13292  lgsval  13505  lgsfvalg  13506  lgsfcl2  13507  lgscllem  13508  lgsval2lem  13511  lgsneg  13525  lgsdir2  13534  lgsdir  13536  lgsdi  13538  lgsne0  13539  lgsdirnn0  13548  lgsdinn0  13549  2sqlem6  13556  sumdc2  13640  pwle2  13838  subctctexmid  13841  nninfsellemeq  13854  exmidsbthrlem  13861