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  7586  ltrel  8387  lerel  8389  frecfzennn  10863  sum0  12155  qnnen  13322  hovercncf  15747  lgsquadlem1  16196  lgsquadlem2  16197  usgrexmpldifpr  16490