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  3193  0disj  4031  disjx0  4033  ontr2exmid  4562  0elsucexmid  4602  relres  4975  cnvdif  5077  funopab4  5296  fun0  5317  fvsn  5760  reltpos  6317  tpostpos  6331  tpos0  6341  oawordriexmid  6537  swoer  6629  xpider  6674  erinxp  6677  domfiexmid  6948  diffitest  6957  pw1dom2  7312  ltrel  8107  lerel  8109  frecfzennn  10537  sum0  11572  qnnen  12675  hovercncf  14968  lgsquadlem1  15404  lgsquadlem2  15405