This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (φ, ψ, χ) \leftrightarrow (φ \land ψ \land χ)$

Step	Hyp	Ref	Expression
0		wph	$wff φ$
1		wps	$wff ψ$
2		wch	$wff χ$
3	0 1 2	wvhc3	$wff (φ, ψ, χ)$
4	0 1 2	w3a	$wff (φ \land ψ \land χ)$
5	3 4	wb	$wff ((φ, ψ, χ) \leftrightarrow (φ \land ψ \land χ))$