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

Metamath Proof Explorer

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 ⊢ φ ψ ↔ φ ∧ ψ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 0 1 wvhc2 wff φ ψ
3 0 1 wa wff φ ∧ ψ
4 2 3 wb wff φ ψ ↔ φ ∧ ψ