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

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  impbii  126  pm3.2i  272  sstri  3257  0disj  4127  disjx0  4129  ontr2exmid  4672  0elsucexmid  4712  relres  5091  cnvdif  5194  funopab4  5414  fun0  5439  fvsn  5910  reltpos  6521  tpostpos  6535  tpos0  6545  oawordriexmid  6743  swoer  6835  xpider  6880  erinxp  6883  domfiexmid  7182  diffitest  7191  pw1dom2  7587  ltrel  8388  lerel  8390  frecfzennn  10878  sum0  12174  qnnen  13374  hovercncf  15838  lgsquadlem1  16362  lgsquadlem2  16363  usgrexmpldifpr  16656