Theorem syl6 29

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)

Hypotheses

Ref	Expression
syl6.1	|- (ph -> (ps -> ch))
syl6.2	|- (ch -> th)

Assertion

Ref	Expression
syl6	|- (ph -> (ps -> th))

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 |- (ph -> (ps -> ch))
2		syl6.2	. . 3 |- (ch -> th)
3	2	a1i 10	. 2 |- (ps -> (ch -> th))
4	1, 3	sylcom 25	1 |- (ph -> (ps -> 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:  syl56  30  syl6com  31  a1dd  42  syl6mpi  58  syl6c  60  com34  77  con1d  116  expi  141  looinv  174  syl6ib  217  syl6ibr  218  syl6bi  219  syl6bir  220  jaoi  368  pm2.37  817  pm2.81  824  oplem1  930  3jao  1243  ee12an  1363  ee23  1364  exlimdv  1636  spimfw  1646  hbald  1740  sp  1747  spOLD  1748  19.23t  1800  hbimdOLD  1816  nfaldOLD  1853  19.21tOLD  1863  ax12olem1  1927  ax12olem2  1928  ax10lem2  1937  ax10lem4  1941  ax10  1944  a16g  1945  spimt  1974  cbv1h  1978  cbv2h  1980  equvini  1987  sbft  2025  sbied  2036  sb3  2052  dfsb2  2055  hbsb2  2057  sbn  2062  sbi1  2063  sb9i  2094  sbal1  2126  aev-o  2182  ax11eq  2193  ax11el  2194  ax11indn  2195  ax11indi  2196  mo  2226  moexex  2273  2mo  2282  2eu1  2284  dvelimdc  2510  rsp2  2677  rgen2a  2681  mo2icl  3016  reu6  3026  reupick2  3542  pwpw0  3856  sssn  3865  pwsnALT  3883  dfiun2g  4000  iotaval  4351  nnsucelr  4429  nndisjeq  4430  ltfintri  4467  tfin11  4494  tfinnn  4535  vfinspss  4552  copsexg  4608  opelopabt  4700  xpcan  5058  xpcan2  5059  fun11iun  5306  fv3  5342  chfnrn  5400  dff3  5421  ffnfv  5428  fconstfv  5457  funsi  5521  oprabid  5551  mpt2eq123  5662  fundmen  6044  enmap2lem4  6067  enmap1lem4  6073  enprmaplem5  6081  leconnnc  6219  addceq0  6220  ncslesuc  6268  nchoicelem6  6295  nchoicelem12  6301  dmfrec  6317