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 φ ψ χ φ ψ χ

Detailed syntax breakdown

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 φ ψ χ
5 3 4 wb wff φ ψ χ φ ψ χ