Theorem e222 39809

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

Syntax hints:   → wi 4   ∧ wa 386  (   wvd2 39741

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 199  df-an 387  df-vd2 39742

This theorem is referenced by:  e220  39810  e202  39812  e022  39814  e002  39816  e020  39818  e200  39820  e221  39822  e212  39824  e122  39826  e112  39827  e121  39829  e211  39830  e22  39844  suctrALT2VD  40009  en3lplem2VD  40017  19.21a3con13vVD  40025  tratrbVD  40034