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	|- ( (. ph ,. ps ). <-> ( ph /\ ps ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2	0 1	wvhc2	|- (. ph ,. ps ).
3	0 1	wa	|- ( ph /\ ps )
4	2 3	wb	|- ( (. ph ,. ps ). <-> ( ph /\ ps ) )