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

Definition df-bnj17 28952
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 28951 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 936 . . 3  wff  ( ph  /\ 
ps  /\  ch )
76, 4wa 359 . 2  wff  ( (
ph  /\  ps  /\  ch )  /\  th )
85, 7wb 177 1  wff  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ( ph  /\  ps  /\  ch )  /\  th ) )
Colors of variables: wff set class
This definition is referenced by:  bnj248  28965  bnj250  28966  bnj258  28973  bnj268  28974  bnj291  28976  bnj312  28977  bnj446  28982  bnj645  29019  bnj658  29020  bnj887  29035  bnj919  29037  bnj945  29045  bnj951  29047  bnj982  29050  bnj1019  29051  bnj518  29158  bnj557  29173  bnj571  29178  bnj594  29184  bnj916  29205  bnj966  29216  bnj967  29217  bnj1006  29231  bnj1018  29234  bnj1040  29242  bnj1174  29273  bnj1175  29274  bnj1311  29294
  Copyright terms: Public domain W3C validator