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 34159
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 34158 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 971 . . 3  wff  ( ph  /\ 
ps  /\  ch )
76, 4wa 367 . 2  wff  ( (
ph  /\  ps  /\  ch )  /\  th )
85, 7wb 184 1  wff  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ( ph  /\  ps  /\  ch )  /\  th ) )
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  34172  bnj250  34173  bnj258  34180  bnj268  34181  bnj291  34183  bnj312  34184  bnj446  34189  bnj645  34227  bnj658  34228  bnj887  34243  bnj919  34245  bnj945  34252  bnj951  34254  bnj982  34257  bnj1019  34258  bnj518  34364  bnj571  34384  bnj594  34390  bnj916  34411  bnj966  34422  bnj967  34423  bnj1006  34437  bnj1018  34440  bnj1040  34448  bnj1174  34479  bnj1175  34480  bnj1311  34500
  Copyright terms: Public domain W3C validator