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  3234  0disj  4083  disjx0  4085  ontr2exmid  4621  0elsucexmid  4661  relres  5039  cnvdif  5141  funopab4  5361  fun0  5385  fvsn  5844  reltpos  6411  tpostpos  6425  tpos0  6435  oawordriexmid  6633  swoer  6725  xpider  6770  erinxp  6773  domfiexmid  7060  diffitest  7069  pw1dom2  7435  ltrel  8231  lerel  8233  frecfzennn  10678  sum0  11939  qnnen  13042  hovercncf  15360  lgsquadlem1  15796  lgsquadlem2  15797  usgrexmpldifpr  16088