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  3251  0disj  4111  disjx0  4113  ontr2exmid  4652  0elsucexmid  4692  relres  5071  cnvdif  5174  funopab4  5394  fun0  5419  fvsn  5884  reltpos  6494  tpostpos  6508  tpos0  6518  oawordriexmid  6716  swoer  6808  xpider  6853  erinxp  6856  domfiexmid  7148  diffitest  7157  pw1dom2  7550  ltrel  8351  lerel  8353  frecfzennn  10815  sum0  12102  qnnen  13269  hovercncf  15640  lgsquadlem1  16079  lgsquadlem2  16080  usgrexmpldifpr  16373