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

Definition df-bnj17 29540
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 29539 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 991 . . 3  wff  ( ph  /\ 
ps  /\  ch )
76, 4wa 375 . 2  wff  ( (
ph  /\  ps  /\  ch )  /\  th )
85, 7wb 189 1  wff  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ( ph  /\  ps  /\  ch )  /\  th ) )
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  29553  bnj250  29554  bnj258  29561  bnj268  29562  bnj291  29564  bnj312  29565  bnj446  29570  bnj645  29608  bnj658  29609  bnj887  29624  bnj919  29626  bnj945  29633  bnj951  29635  bnj982  29638  bnj1019  29639  bnj518  29745  bnj571  29765  bnj594  29771  bnj916  29792  bnj966  29803  bnj967  29804  bnj1006  29818  bnj1018  29821  bnj1040  29829  bnj1174  29860  bnj1175  29861  bnj1311  29881
  Copyright terms: Public domain W3C validator