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 33447
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 33446 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 972 . . 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  33460  bnj250  33461  bnj258  33468  bnj268  33469  bnj291  33471  bnj312  33472  bnj446  33477  bnj645  33514  bnj658  33515  bnj887  33530  bnj919  33532  bnj945  33539  bnj951  33541  bnj982  33544  bnj1019  33545  bnj518  33651  bnj571  33671  bnj594  33677  bnj916  33698  bnj966  33709  bnj967  33710  bnj1006  33724  bnj1018  33727  bnj1040  33735  bnj1174  33766  bnj1175  33767  bnj1311  33787
  Copyright terms: Public domain W3C validator