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 32819
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 32818 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 973 . . 3  wff  ( ph  /\ 
ps  /\  ch )
76, 4wa 369 . 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  32832  bnj250  32833  bnj258  32840  bnj268  32841  bnj291  32843  bnj312  32844  bnj446  32849  bnj645  32886  bnj658  32887  bnj887  32902  bnj919  32904  bnj945  32911  bnj951  32913  bnj982  32916  bnj1019  32917  bnj518  33023  bnj557  33038  bnj571  33043  bnj594  33049  bnj916  33070  bnj966  33081  bnj967  33082  bnj1006  33096  bnj1018  33099  bnj1040  33107  bnj1174  33138  bnj1175  33139  bnj1311  33159
  Copyright terms: Public domain W3C validator