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 29488
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 29487 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 982 . . 3  wff  ( ph  /\ 
ps  /\  ch )
76, 4wa 370 . 2  wff  ( (
ph  /\  ps  /\  ch )  /\  th )
85, 7wb 187 1  wff  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ( ph  /\  ps  /\  ch )  /\  th ) )
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  29501  bnj250  29502  bnj258  29509  bnj268  29510  bnj291  29512  bnj312  29513  bnj446  29518  bnj645  29556  bnj658  29557  bnj887  29572  bnj919  29574  bnj945  29581  bnj951  29583  bnj982  29586  bnj1019  29587  bnj518  29693  bnj571  29713  bnj594  29719  bnj916  29740  bnj966  29751  bnj967  29752  bnj1006  29766  bnj1018  29769  bnj1040  29777  bnj1174  29808  bnj1175  29809  bnj1311  29829
  Copyright terms: Public domain W3C validator