Theorem e222 45423

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

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

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 45365

This theorem is used by:  e220  45424  e202  45426  e022  45428  e002  45430  e020  45432  e200  45434  e221  45436  e212  45438  e122  45440  e112  45441  e121  45443  e211  45444  e22  45458  suctrALT2VD  45622  en3lplem2VD  45630  19.21a3con13vVD  45638  tratrbVD  45647