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  3189  0disj  4027  disjx0  4029  ontr2exmid  4558  0elsucexmid  4598  relres  4971  cnvdif  5073  funopab4  5292  fun0  5313  fvsn  5754  reltpos  6305  tpostpos  6319  tpos0  6329  oawordriexmid  6525  swoer  6617  xpider  6662  erinxp  6665  domfiexmid  6936  diffitest  6945  pw1dom2  7289  ltrel  8083  lerel  8085  frecfzennn  10500  sum0  11534  qnnen  12591  hovercncf  14825  lgsquadlem1  15234  lgsquadlem2  15235