Definition df-vd2

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	0 1 2	wvd2	⊢ (    𝜑    ,    𝜓    ▶    𝜒    )
4	0 1	wa	⊢ ( 𝜑 ∧ 𝜓 )
5	4 2	wi	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
6	3 5	wb	⊢ ( (    𝜑    ,    𝜓    ▶    𝜒    ) ↔ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) )