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  125  pm3.2i  267  sstri  3037  0disj  3850  disjx0  3852  ontr2exmid  4356  0elsucexmid  4396  relres  4756  cnvdif  4853  funopab4  5066  fun0  5087  fvsn  5508  reltpos  6031  tpostpos  6045  tpos0  6055  oawordriexmid  6247  swoer  6336  xpiderm  6379  erinxp  6382  domfiexmid  6650  diffitest  6659  ltrel  7611  lerel  7613  frecfzennn  9896  sum0  10843  pw1dom2  12193