Theorem e222 45619

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

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

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 45561

This theorem is used by:  e220  45620  e202  45622  e022  45624  e002  45626  e020  45628  e200  45630  e221  45632  e212  45634  e122  45636  e112  45637  e121  45639  e211  45640  e22  45654  suctrALT2VD  45818  en3lplem2VD  45826  19.21a3con13vVD  45834  tratrbVD  45843