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  3166  0disj  4002  disjx0  4004  ontr2exmid  4526  0elsucexmid  4566  relres  4937  cnvdif  5037  funopab4  5255  fun0  5276  fvsn  5713  reltpos  6253  tpostpos  6267  tpos0  6277  oawordriexmid  6473  swoer  6565  xpider  6608  erinxp  6611  domfiexmid  6880  diffitest  6889  pw1dom2  7228  ltrel  8021  lerel  8023  frecfzennn  10428  sum0  11398  qnnen  12434