Theorem e222 44819

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 44768	. . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏))
3	2	imp 406	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
4		e222.1	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
5	4	dfvd2i 44768	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒))
6	5	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
7		e222.2	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
8	7	dfvd2i 44768	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜃))
9	8	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
10		e222.4	. . . . . . 7 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))
11	6, 9, 10	syl2im 40	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → (𝜏 → 𝜂)))
12	11	pm2.43i 52	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝜏 → 𝜂))
13	3, 12	syl5com 31	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → 𝜂))
14	13	pm2.43i 52	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
15	14	ex 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜂))
16	15	dfvd2ir 44769	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )

Syntax hints:   → wi 4   ∧ wa 395  (   wvd2 44760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-vd2 44761

This theorem is referenced by:  e220  44820  e202  44822  e022  44824  e002  44826  e020  44828  e200  44830  e221  44832  e212  44834  e122  44836  e112  44837  e121  44839  e211  44840  e22  44854  suctrALT2VD  45018  en3lplem2VD  45026  19.21a3con13vVD  45034  tratrbVD  45043