Definition df-vhc2 42154

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

Assertion

Ref	Expression
df-vhc2	⊢ ((   𝜑   ,   𝜓   ) ↔ (𝜑 ∧ 𝜓))

Detailed syntax breakdown of Definition df-vhc2

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wvhc2 42153	. 2 wff (   𝜑   ,   𝜓   )
4	1, 2	wa 395	. 2 wff (𝜑 ∧ 𝜓)
5	3, 4	wb 205	1 wff ((   𝜑   ,   𝜓   ) ↔ (𝜑 ∧ 𝜓))

This definition is referenced by:  dfvd2an  42155