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 31562
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 31561 . 2  wff  ( ph  /\ 
ps  /\  ch  /\  th )
61, 2, 3w3a 965 . . 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  31575  bnj250  31576  bnj258  31583  bnj268  31584  bnj291  31586  bnj312  31587  bnj446  31592  bnj645  31629  bnj658  31630  bnj887  31645  bnj919  31647  bnj945  31654  bnj951  31656  bnj982  31659  bnj1019  31660  bnj518  31766  bnj557  31781  bnj571  31786  bnj594  31792  bnj916  31813  bnj966  31824  bnj967  31825  bnj1006  31839  bnj1018  31842  bnj1040  31850  bnj1174  31881  bnj1175  31882  bnj1311  31902
  Copyright terms: Public domain W3C validator