Definition df-vd3

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3		wth	⊢ 𝜃
4	0 1 2 3	wvd3	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    )
5	0 1 2	w3a	⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 )
6	5 3	wi	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
7	4 6	wb	⊢ ( (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 ) )