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  125  pm3.2i  270  sstri  3151  0disj  3979  disjx0  3981  ontr2exmid  4502  0elsucexmid  4542  relres  4912  cnvdif  5010  funopab4  5225  fun0  5246  fvsn  5680  reltpos  6218  tpostpos  6232  tpos0  6242  oawordriexmid  6438  swoer  6529  xpider  6572  erinxp  6575  domfiexmid  6844  diffitest  6853  pw1dom2  7183  ltrel  7960  lerel  7962  frecfzennn  10361  sum0  11329  qnnen  12364