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  3192  0disj  4030  disjx0  4032  ontr2exmid  4561  0elsucexmid  4601  relres  4974  cnvdif  5076  funopab4  5295  fun0  5316  fvsn  5757  reltpos  6308  tpostpos  6322  tpos0  6332  oawordriexmid  6528  swoer  6620  xpider  6665  erinxp  6668  domfiexmid  6939  diffitest  6948  pw1dom2  7294  ltrel  8088  lerel  8090  frecfzennn  10518  sum0  11553  qnnen  12648  hovercncf  14882  lgsquadlem1  15318  lgsquadlem2  15319