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 31978
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 31977 . 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  31991  bnj250  31992  bnj258  31999  bnj268  32000  bnj291  32002  bnj312  32003  bnj446  32008  bnj645  32045  bnj658  32046  bnj887  32061  bnj919  32063  bnj945  32070  bnj951  32072  bnj982  32075  bnj1019  32076  bnj518  32182  bnj557  32197  bnj571  32202  bnj594  32208  bnj916  32229  bnj966  32240  bnj967  32241  bnj1006  32255  bnj1018  32258  bnj1040  32266  bnj1174  32297  bnj1175  32298  bnj1311  32318
  Copyright terms: Public domain W3C validator