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  3164  0disj  3999  disjx0  4001  ontr2exmid  4523  0elsucexmid  4563  relres  4934  cnvdif  5034  funopab4  5252  fun0  5273  fvsn  5710  reltpos  6248  tpostpos  6262  tpos0  6272  oawordriexmid  6468  swoer  6560  xpider  6603  erinxp  6606  domfiexmid  6875  diffitest  6884  pw1dom2  7223  ltrel  8015  lerel  8017  frecfzennn  10421  sum0  11389  qnnen  12424