Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnj17 Unicode version

Definition df-bnj17 28712
Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
df-bnj17  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ( ph  /\  ps  /\  ch )  /\  th ) )

Detailed syntax breakdown of Definition df-bnj17
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
4 wth . . 3  wff  th
51, 2, 3, 4w-bnj17 28711 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 934 . . 3  wff  ( ph  /\ 
ps  /\  ch )
76, 4wa 358 . 2  wff  ( (
ph  /\  ps  /\  ch )  /\  th )
85, 7wb 176 1  wff  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ( ph  /\  ps  /\  ch )  /\  th ) )
Colors of variables: wff set class
This definition is referenced by:  bnj248  28725  bnj250  28726  bnj258  28733  bnj268  28734  bnj291  28736  bnj312  28737  bnj446  28742  bnj645  28779  bnj658  28780  bnj887  28795  bnj919  28797  bnj945  28805  bnj951  28807  bnj982  28810  bnj1019  28811  bnj518  28918  bnj557  28933  bnj571  28938  bnj594  28944  bnj916  28965  bnj966  28976  bnj967  28977  bnj1006  28991  bnj1018  28994  bnj1040  29002  bnj1174  29033  bnj1175  29034  bnj1311  29054
  Copyright terms: Public domain W3C validator