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  3203  0disj  4044  disjx0  4046  ontr2exmid  4577  0elsucexmid  4617  relres  4992  cnvdif  5094  funopab4  5313  fun0  5337  fvsn  5786  reltpos  6343  tpostpos  6357  tpos0  6367  oawordriexmid  6563  swoer  6655  xpider  6700  erinxp  6703  domfiexmid  6982  diffitest  6991  pw1dom2  7346  ltrel  8141  lerel  8143  frecfzennn  10578  sum0  11743  qnnen  12846  hovercncf  15162  lgsquadlem1  15598  lgsquadlem2  15599