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 29028
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 29027 . 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  29041  bnj250  29042  bnj258  29049  bnj268  29050  bnj291  29052  bnj312  29053  bnj446  29058  bnj645  29095  bnj658  29096  bnj887  29111  bnj919  29113  bnj945  29121  bnj951  29123  bnj982  29126  bnj1019  29127  bnj518  29234  bnj557  29249  bnj571  29254  bnj594  29260  bnj916  29281  bnj966  29292  bnj967  29293  bnj1006  29307  bnj1018  29310  bnj1040  29318  bnj1174  29349  bnj1175  29350  bnj1311  29370
  Copyright terms: Public domain W3C validator