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  3257  0disj  4122  disjx0  4124  ontr2exmid  4667  0elsucexmid  4707  relres  5086  cnvdif  5189  funopab4  5409  fun0  5434  fvsn  5901  reltpos  6511  tpostpos  6525  tpos0  6535  oawordriexmid  6733  swoer  6825  xpider  6870  erinxp  6873  domfiexmid  7172  diffitest  7181  pw1dom2  7576  ltrel  8377  lerel  8379  frecfzennn  10841  sum0  12133  qnnen  13300  hovercncf  15670  lgsquadlem1  16110  lgsquadlem2  16111  usgrexmpldifpr  16404