Definition df-vhc3

Description: Definition of a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Assertion	df-vhc3	|- ( (. ph ,. ps ,. ch ). <-> ( ph /\ ps /\ ch ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3	0 1 2	wvhc3	|- (. ph ,. ps ,. ch ).
4	0 1 2	w3a	|- ( ph /\ ps /\ ch )
5	3 4	wb	|- ( (. ph ,. ps ,. ch ). <-> ( ph /\ ps /\ ch ) )