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  3009  0disj  3790  disjx0  3792  ontr2exmid  4276  0elsucexmid  4316  relres  4667  cnvdif  4760  funopab4  4967  fun0  4988  fvsn  5390  reltpos  5899  tpostpos  5913  tpos0  5923  oawordriexmid  6114  swoer  6200  xpiderm  6243  erinxp  6246  domfiexmid  6413  diffitest  6421  ltrel  7241  lerel  7243  frecfzennn  9508