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  3236  0disj  4085  disjx0  4087  ontr2exmid  4623  0elsucexmid  4663  relres  5041  cnvdif  5143  funopab4  5363  fun0  5388  fvsn  5848  reltpos  6415  tpostpos  6429  tpos0  6439  oawordriexmid  6637  swoer  6729  xpider  6774  erinxp  6777  domfiexmid  7066  diffitest  7075  pw1dom2  7444  ltrel  8240  lerel  8242  frecfzennn  10687  sum0  11948  qnnen  13051  hovercncf  15369  lgsquadlem1  15805  lgsquadlem2  15806  usgrexmpldifpr  16099