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  3234  0disj  4081  disjx0  4083  ontr2exmid  4619  0elsucexmid  4659  relres  5037  cnvdif  5139  funopab4  5359  fun0  5383  fvsn  5842  reltpos  6409  tpostpos  6423  tpos0  6433  oawordriexmid  6631  swoer  6723  xpider  6768  erinxp  6771  domfiexmid  7058  diffitest  7067  pw1dom2  7433  ltrel  8229  lerel  8231  frecfzennn  10676  sum0  11936  qnnen  13039  hovercncf  15357  lgsquadlem1  15793  lgsquadlem2  15794  usgrexmpldifpr  16084