Theorem sylc 61

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 48	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  62  mpsyl  64  imp  122  2thd  173  jca  300  syl2anc  403  jc  612  annimdc  878  orandc  880  dn1dc  901  syl2an23an  1230  xordidc  1330  nfimd  1517  exlimd2  1526  elex22  2614  elex2  2615  spcimdv  2682  spcimedv  2684  rspcda  2706  spsbcd  2827  opth  3992  euotd  4009  ssorduni  4231  wetriext  4319  tfisi  4328  sotri2  4742  sotri3  4743  unielrel  4865  funmo  4937  fnfvima  5414  fliftfun  5456  fliftval  5460  riota5f  5512  riotass2  5514  grprinvlem  5715  grprinvd  5716  caofref  5752  tfrlem1  5946  tfrlem5  5953  tfrlemibxssdm  5964  tfrlemibfn  5965  tfrlemiex  5968  rdgisucinc  5995  frecabex  6007  ertr  6144  qliftlem  6207  th3q  6234  f1dom2g  6259  dom3d  6277  en1  6302  xpdom3m  6331  phplem4dom  6348  phpm  6351  phpelm  6352  findcard  6372  f1dmvrnfibi  6393  suplub2ti  6414  supelti  6415  ordiso2  6446  recexnq  6580  ltbtwnnqq  6605  addnnnq0  6639  mulnnnq0  6640  prltlu  6677  prarloclemn  6689  prarloc  6693  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  ltexprlemrl  6800  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprprlemml  6884  addsrpr  6922  mulsrpr  6923  axcaucvglemres  7065  lemul12a  7940  lemulge11  7944  nngt0  8064  nn0ge0  8313  nn0ge2m1nn  8348  zletric  8395  zlelttric  8396  nn0n0n1ge2b  8427  nn0ind-raph  8464  supinfneg  8683  infsupneg  8684  rpge0  8746  fz0fzelfz0  9138  fz0fzdiffz0  9141  ige2m2fzo  9207  elfzodifsumelfzo  9210  elfzom1elp1fzo  9211  exfzdc  9249  qletric  9253  qlelttric  9254  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  frecuzrdgfn  9414  frecuzrdg0  9416  frecfzennn  9419  iseqovex  9439  iseqfn  9441  iseq1  9442  iseqcl  9443  iseqp1  9445  iseqfveq2  9448  iseqfveq  9450  iseqshft2  9452  monoord  9455  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqid3s  9466  iseqid  9467  iseqhomo  9468  expcl2lemap  9488  leexp1a  9531  expnbnd  9596  faclbnd  9668  faclbnd6  9671  facavg  9673  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemdecn  9898  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  qabsor  9961  cau3lem  10000  climi  10126  climcn1  10147  climcn2  10148  dvdsleabs2  10246  4dvdseven  10317  gcdmndc  10340  zsupcllemstep  10341  infssuzex  10345  gcdsupex  10349  gcdsupcl  10350  gcdeq0  10368  gcdaddm  10375  bezoutlemmain  10387  rppwr  10417  ialgfx  10434  eucialgcvga  10440  lcmmndc  10444  lcmval  10445  lcmcllem  10449  lcmledvds  10452  lcmeq0  10453  qredeq  10478  isprm3  10500  prmind2  10502  rpexp  10532  sqpweven  10553  2sqpwodd  10554