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  3247  0disj  4106  disjx0  4108  ontr2exmid  4647  0elsucexmid  4687  relres  5066  cnvdif  5169  funopab4  5389  fun0  5414  fvsn  5879  reltpos  6481  tpostpos  6495  tpos0  6505  oawordriexmid  6703  swoer  6795  xpider  6840  erinxp  6843  domfiexmid  7135  diffitest  7144  pw1dom2  7537  ltrel  8335  lerel  8337  frecfzennn  10788  sum0  12074  qnnen  13182  hovercncf  15511  lgsquadlem1  15950  lgsquadlem2  15951  usgrexmpldifpr  16244