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  3235  0disj  4086  disjx0  4088  ontr2exmid  4625  0elsucexmid  4665  relres  5043  cnvdif  5145  funopab4  5365  fun0  5390  fvsn  5852  reltpos  6421  tpostpos  6435  tpos0  6445  oawordriexmid  6643  swoer  6735  xpider  6780  erinxp  6783  domfiexmid  7072  diffitest  7081  pw1dom2  7450  ltrel  8246  lerel  8248  frecfzennn  10694  sum0  11972  qnnen  13075  hovercncf  15399  lgsquadlem1  15835  lgsquadlem2  15836  usgrexmpldifpr  16129