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
|- ( (. 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 ) )