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  3233  0disj  4080  disjx0  4082  ontr2exmid  4617  0elsucexmid  4657  relres  5033  cnvdif  5135  funopab4  5355  fun0  5379  fvsn  5838  reltpos  6402  tpostpos  6416  tpos0  6426  oawordriexmid  6624  swoer  6716  xpider  6761  erinxp  6764  domfiexmid  7048  diffitest  7057  pw1dom2  7423  ltrel  8219  lerel  8221  frecfzennn  10660  sum0  11914  qnnen  13017  hovercncf  15335  lgsquadlem1  15771  lgsquadlem2  15772