Theorem e222 45524

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e222.1	⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
e222.2	⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
e222.3	⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
e222.4	⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))

Assertion

Ref	Expression
e222	⊢ (   𝜑   ,   𝜓   ▶   𝜂   )

Proof of Theorem e222

Step	Hyp	Ref	Expression
1		e222.3	. . . . . . 7 ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
2	1	dfvd2i 45473	. . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏))
3	2	imp 412	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
4		e222.1	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
5	4	dfvd2i 45473	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒))
6	5	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
7		e222.2	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
8	7	dfvd2i 45473	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜃))
9	8	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
10		e222.4	. . . . . . 7 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))
11	6, 9, 10	syl2im 41	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → (𝜏 → 𝜂)))
12	11	pm2.43i 53	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝜏 → 𝜂))
13	3, 12	syl5com 32	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → 𝜂))
14	13	pm2.43i 53	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
15	14	ex 418	. 2 ⊢ (𝜑 → (𝜓 → 𝜂))
16	15	dfvd2ir 45474	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  (   wvd2 45465

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

This proof depends on definitions:  df-bi 210  df-an 402  df-vd2 45466

This theorem is used by:  e220  45525  e202  45527  e022  45529  e002  45531  e020  45533  e200  45535  e221  45537  e212  45539  e122  45541  e112  45542  e121  45544  e211  45545  e22  45559  suctrALT2VD  45723  en3lplem2VD  45731  19.21a3con13vVD  45739  tratrbVD  45748