Definition df-vd1

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

	Ref	Expression
Assertion	df-vd1	$$⊢\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \psi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wvd1	$$wff\left(\phi \to \psi \right)$$
3	0 1	wi	$$wff\left(\phi \to \psi \right)$$
4	2 3	wb	$$wff\left(\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \psi \right)\right)$$