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 28390
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 28389 . 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  28403  bnj250  28404  bnj258  28411  bnj268  28412  bnj291  28414  bnj312  28415  bnj446  28420  bnj645  28457  bnj658  28458  bnj887  28473  bnj919  28475  bnj945  28483  bnj951  28485  bnj982  28488  bnj1019  28489  bnj518  28596  bnj557  28611  bnj571  28616  bnj594  28622  bnj916  28643  bnj966  28654  bnj967  28655  bnj1006  28669  bnj1018  28672  bnj1040  28680  bnj1174  28711  bnj1175  28712  bnj1311  28732
  Copyright terms: Public domain W3C validator