Definition df-vd3 42210

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

Assertion

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

Detailed syntax breakdown of Definition df-vd3

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4		wth	. . 3 wff 𝜃
5	1, 2, 3, 4	wvd3 42207	. 2 wff (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )
6	1, 2, 3	w3a 1086	. . 3 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
7	6, 4	wi 4	. 2 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
8	5, 7	wb 205	1 wff ((   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   ) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃))

This definition is referenced by:  dfvd3  42211