Theorem e222 45808

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 45757	. . . . . 6 ⊢ (𝜑 → (𝜓 → 𝜏))
3	2	imp 412	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
4		e222.1	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
5	4	dfvd2i 45757	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → 𝜒))
6	5	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
7		e222.2	. . . . . . . . 9 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
8	7	dfvd2i 45757	. . . . . . . 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 45758	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )

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

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 45750

This theorem is used by:  e220  45809  e202  45811  e022  45813  e002  45815  e020  45817  e200  45819  e221  45821  e212  45823  e122  45825  e112  45826  e121  45828  e211  45829  e22  45843  suctrALT2VD  46007  en3lplem2VD  46015  19.21a3con13vVD  46023  tratrbVD  46032