Definition df-vhc2

Description: Definition of a 2-element virtual hypotheses collection. (Contributed by Alan Sare, 23-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Assertion	df-vhc2	$$⊢\left(\phi ,\psi \right)\leftrightarrow \left(\phi \wedge \psi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wvhc2	$$wff\left(\phi ,\psi \right)$$
3	0 1	wa	$$wff\left(\phi \wedge \psi \right)$$
4	2 3	wb	$$wff\left(\left(\phi ,\psi \right)\leftrightarrow \left(\phi \wedge \psi \right)\right)$$