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  3106  0disj  3926  disjx0  3928  ontr2exmid  4440  0elsucexmid  4480  relres  4847  cnvdif  4945  funopab4  5160  fun0  5181  fvsn  5615  reltpos  6147  tpostpos  6161  tpos0  6171  oawordriexmid  6366  swoer  6457  xpider  6500  erinxp  6503  domfiexmid  6772  diffitest  6781  ltrel  7826  lerel  7828  frecfzennn  10199  sum0  11157  qnnen  11944  pw1dom2  13190