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	⊢ 𝜑
mp2.2	⊢ 𝜓
mp2.3	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mp2	⊢ 𝜒

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.1	. 2 ⊢ 𝜑
2		mp2.2	. . 3 ⊢ 𝜓
3		mp2.3	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpi 15	. 2 ⊢ (𝜑 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

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  3213  0disj  4059  disjx0  4061  ontr2exmid  4594  0elsucexmid  4634  relres  5009  cnvdif  5111  funopab4  5331  fun0  5355  fvsn  5807  reltpos  6366  tpostpos  6380  tpos0  6390  oawordriexmid  6586  swoer  6678  xpider  6723  erinxp  6726  domfiexmid  7008  diffitest  7017  pw1dom2  7380  ltrel  8176  lerel  8178  frecfzennn  10615  sum0  11865  qnnen  12968  hovercncf  15285  lgsquadlem1  15721  lgsquadlem2  15722