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  3237  0disj  4090  disjx0  4092  ontr2exmid  4629  0elsucexmid  4669  relres  5047  cnvdif  5150  funopab4  5370  fun0  5395  fvsn  5857  reltpos  6459  tpostpos  6473  tpos0  6483  oawordriexmid  6681  swoer  6773  xpider  6818  erinxp  6821  domfiexmid  7110  diffitest  7119  pw1dom2  7488  ltrel  8283  lerel  8285  frecfzennn  10734  sum0  12012  qnnen  13115  hovercncf  15440  lgsquadlem1  15879  lgsquadlem2  15880  usgrexmpldifpr  16173