Theorem mp2 16

Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses

Ref	Expression
mp2.1	|- ph
mp2.2	|- ps
mp2.3	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mp2	|- ch

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.1	. 2 |- ph
2		mp2.2	. . 3 |- ps
3		mp2.3	. . 3 |- ( ph -> ( ps -> ch ) )
4	2, 3	mpi 15	. 2 |- ( ph -> ch )
5	1, 4	ax-mp 5	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  impbii  126  pm3.2i  272  sstri  3201  0disj  4040  disjx0  4042  ontr2exmid  4572  0elsucexmid  4612  relres  4986  cnvdif  5088  funopab4  5307  fun0  5331  fvsn  5778  reltpos  6335  tpostpos  6349  tpos0  6359  oawordriexmid  6555  swoer  6647  xpider  6692  erinxp  6695  domfiexmid  6974  diffitest  6983  pw1dom2  7338  ltrel  8133  lerel  8135  frecfzennn  10569  sum0  11641  qnnen  12744  hovercncf  15060  lgsquadlem1  15496  lgsquadlem2  15497