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  4127  disjx0  4129  ontr2exmid  4672  0elsucexmid  4712  relres  5091  cnvdif  5194  funopab4  5414  fun0  5439  fvsn  5910  reltpos  6521  tpostpos  6535  tpos0  6545  oawordriexmid  6743  swoer  6835  xpider  6880  erinxp  6883  domfiexmid  7182  diffitest  7191  pw1dom2  7586  ltrel  8387  lerel  8389  frecfzennn  10865  sum0  12157  qnnen  13324  hovercncf  15749  lgsquadlem1  16208  lgsquadlem2  16209  usgrexmpldifpr  16502