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  3101  0disj  3921  disjx0  3923  ontr2exmid  4435  0elsucexmid  4475  relres  4842  cnvdif  4940  funopab4  5155  fun0  5176  fvsn  5608  reltpos  6140  tpostpos  6154  tpos0  6164  oawordriexmid  6359  swoer  6450  xpider  6493  erinxp  6496  domfiexmid  6765  diffitest  6774  ltrel  7819  lerel  7821  frecfzennn  10192  sum0  11150  qnnen  11933  pw1dom2  13179