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