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  3233  0disj  4079  disjx0  4081  ontr2exmid  4616  0elsucexmid  4656  relres  5032  cnvdif  5134  funopab4  5354  fun0  5378  fvsn  5833  reltpos  6394  tpostpos  6408  tpos0  6418  oawordriexmid  6614  swoer  6706  xpider  6751  erinxp  6754  domfiexmid  7036  diffitest  7045  pw1dom2  7408  ltrel  8204  lerel  8206  frecfzennn  10643  sum0  11894  qnnen  12997  hovercncf  15314  lgsquadlem1  15750  lgsquadlem2  15751