Theorem e222 37882

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

Syntax hints:   → wi 4   ∧ wa 383  (   wvd2 37814

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 196  df-an 385  df-vd2 37815

This theorem is referenced by:  e220  37883  e202  37885  e022  37887  e002  37889  e020  37891  e200  37893  e221  37895  e212  37897  e122  37899  e112  37900  e121  37902  e211  37903  e22  37917  suctrALT2VD  38093  en3lplem2VD  38101  19.21a3con13vVD  38109  tratrbVD  38119