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  3206  0disj  4048  disjx0  4050  ontr2exmid  4581  0elsucexmid  4621  relres  4996  cnvdif  5098  funopab4  5317  fun0  5341  fvsn  5792  reltpos  6349  tpostpos  6363  tpos0  6373  oawordriexmid  6569  swoer  6661  xpider  6706  erinxp  6709  domfiexmid  6990  diffitest  6999  pw1dom2  7358  ltrel  8154  lerel  8156  frecfzennn  10593  sum0  11774  qnnen  12877  hovercncf  15193  lgsquadlem1  15629  lgsquadlem2  15630