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  3164  0disj  3998  disjx0  4000  ontr2exmid  4522  0elsucexmid  4562  relres  4932  cnvdif  5032  funopab4  5250  fun0  5271  fvsn  5708  reltpos  6246  tpostpos  6260  tpos0  6270  oawordriexmid  6466  swoer  6558  xpider  6601  erinxp  6604  domfiexmid  6873  diffitest  6882  pw1dom2  7221  ltrel  8013  lerel  8015  frecfzennn  10419  sum0  11387  qnnen  12422