Definition df-vd1

Description: Definition of virtual deduction. (Contributed by Alan Sare, 21-Apr-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	df-vd1	⊢ ( (    𝜑    ▶    𝜓    ) ↔ ( 𝜑 → 𝜓 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2	0 1	wvd1	⊢ (    𝜑    ▶    𝜓    )
3	0 1	wi	⊢ ( 𝜑 → 𝜓 )
4	2 3	wb	⊢ ( (    𝜑    ▶    𝜓    ) ↔ ( 𝜑 → 𝜓 ) )