Definition df-vd2 42087

Description: Definition of a 2-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
df-vd2	⊢ ((   𝜑   ,   𝜓   ▶   𝜒   ) ↔ ((𝜑 ∧ 𝜓) → 𝜒))

Detailed syntax breakdown of Definition df-vd2

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	wvd2 42086	. 2 wff (   𝜑   ,   𝜓   ▶   𝜒   )
5	1, 2	wa 395	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wi 4	. 2 wff ((𝜑 ∧ 𝜓) → 𝜒)
7	4, 6	wb 205	1 wff ((   𝜑   ,   𝜓   ▶   𝜒   ) ↔ ((𝜑 ∧ 𝜓) → 𝜒))

This definition is referenced by:  dfvd2  42088