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	$$⊢\left(\phi ,\psi \to \chi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\to \chi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2		wch	$$wff\chi$$
3	0 1 2	wvd2	$$wff\left(\phi ,\psi \to \chi \right)$$
4	0 1	wa	$$wff\left(\phi \wedge \psi \right)$$
5	4 2	wi	$$wff\left(\left(\phi \wedge \psi \right)\to \chi \right)$$
6	3 5	wb	$$wff\left(\left(\phi ,\psi \to \chi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\to \chi \right)\right)$$