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  3111  0disj  3934  disjx0  3936  ontr2exmid  4448  0elsucexmid  4488  relres  4855  cnvdif  4953  funopab4  5168  fun0  5189  fvsn  5623  reltpos  6155  tpostpos  6169  tpos0  6179  oawordriexmid  6374  swoer  6465  xpider  6508  erinxp  6511  domfiexmid  6780  diffitest  6789  ltrel  7850  lerel  7852  frecfzennn  10230  sum0  11189  qnnen  11980  pw1dom2  13361