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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  impbii  126  pm3.2i  272  sstri  3257  0disj  4128  disjx0  4130  ontr2exmid  4674  0elsucexmid  4714  relres  5093  cnvdif  5197  funopab4  5417  fun0  5442  fvsn  5913  reltpos  6525  tpostpos  6539  tpos0  6549  oawordriexmid  6747  swoer  6839  xpider  6884  erinxp  6887  domfiexmid  7187  diffitest  7196  pw1dom2  7593  ltrel  8394  lerel  8396  frecfzennn  10885  sum0  12181  qnnen  13381  hovercncf  15884  lgsquadlem1  16413  lgsquadlem2  16414  usgrexmpldifpr  16707