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 7	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  impbii  124  pm3.2i  266  sstri  3008  0disj  3782  disjx0  3784  ontr2exmid  4268  0elsucexmid  4308  relres  4657  cnvdif  4750  funopab4  4957  fun0  4977  fvsn  5379  reltpos  5888  tpostpos  5902  tpos0  5912  swoer  6157  xpiderm  6200  erinxp  6203  domfiexmid  6363  diffitest  6371  ltrel  7174  lerel  7176  frecfzennn  9419