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  3188  0disj  4026  disjx0  4028  ontr2exmid  4557  0elsucexmid  4597  relres  4970  cnvdif  5072  funopab4  5291  fun0  5312  fvsn  5753  reltpos  6303  tpostpos  6317  tpos0  6327  oawordriexmid  6523  swoer  6615  xpider  6660  erinxp  6663  domfiexmid  6934  diffitest  6943  pw1dom2  7287  ltrel  8081  lerel  8083  frecfzennn  10497  sum0  11531  qnnen  12588  hovercncf  14800  lgsquadlem1  15191