Theorem e222 45089

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

Syntax hints:   → wi 4   ∧ wa 396  (   wvd2 45030

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 208  df-an 397  df-vd2 45031

This theorem is referenced by:  e220  45090  e202  45092  e022  45094  e002  45096  e020  45098  e200  45100  e221  45102  e212  45104  e122  45106  e112  45107  e121  45109  e211  45110  e22  45124  suctrALT2VD  45288  en3lplem2VD  45296  19.21a3con13vVD  45304  tratrbVD  45313