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  3193  0disj  4031  disjx0  4033  ontr2exmid  4562  0elsucexmid  4602  relres  4975  cnvdif  5077  funopab4  5296  fun0  5317  fvsn  5760  reltpos  6317  tpostpos  6331  tpos0  6341  oawordriexmid  6537  swoer  6629  xpider  6674  erinxp  6677  domfiexmid  6948  diffitest  6957  pw1dom2  7310  ltrel  8105  lerel  8107  frecfzennn  10535  sum0  11570  qnnen  12673  hovercncf  14966  lgsquadlem1  15402  lgsquadlem2  15403