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 7	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  impbii  117  pm3.2i  257  sstri  2954  0disj  3761  disjx0  3763  ontr2exmid  4250  0elsucexmid  4289  relres  4639  cnvdif  4730  funopab4  4937  fun0  4957  fvsn  5358  reltpos  5865  tpostpos  5879  tpos0  5889  swoer  6134  xpiderm  6177  erinxp  6180  diffitest  6344  ltrel  7081  lerel  7083  frecfzennn  9203