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	⊢ ( (    𝜑    ,    𝜓    ) ↔ ( 𝜑 ∧ 𝜓 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2	0 1	wvhc2	⊢ (    𝜑    ,    𝜓    )
3	0 1	wa	⊢ ( 𝜑 ∧ 𝜓 )
4	2 3	wb	⊢ ( (    𝜑    ,    𝜓    ) ↔ ( 𝜑 ∧ 𝜓 ) )