Theorem e222 43397

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 43346	. . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏))
3	2	imp 408	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
4		e222.1	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
5	4	dfvd2i 43346	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒))
6	5	imp 408	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
7		e222.2	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
8	7	dfvd2i 43346	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜃))
9	8	imp 408	. . . . . . 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 414	. 2 ⊢ (𝜑 → (𝜓 → 𝜂))
16	15	dfvd2ir 43347	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )

Syntax hints:   → wi 4   ∧ wa 397  (   wvd2 43338

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 206  df-an 398  df-vd2 43339

This theorem is referenced by:  e220  43398  e202  43400  e022  43402  e002  43404  e020  43406  e200  43408  e221  43410  e212  43412  e122  43414  e112  43415  e121  43417  e211  43418  e22  43432  suctrALT2VD  43597  en3lplem2VD  43605  19.21a3con13vVD  43613  tratrbVD  43622