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

Definition df-bnj17 32067
Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
df-bnj17 ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))

Detailed syntax breakdown of Definition df-bnj17
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
4 wth . . 3 wff 𝜃
51, 2, 3, 4w-bnj17 32066 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1084 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 399 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 209 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  32080  bnj250  32081  bnj258  32088  bnj268  32089  bnj291  32091  bnj312  32092  bnj446  32097  bnj645  32131  bnj658  32132  bnj887  32146  bnj919  32148  bnj945  32155  bnj951  32157  bnj982  32160  bnj1019  32161  bnj518  32268  bnj571  32288  bnj594  32294  bnj916  32315  bnj966  32326  bnj967  32327  bnj1006  32342  bnj1018g  32345  bnj1018  32346  bnj1040  32354  bnj1174  32385  bnj1175  32386  bnj1311  32406
  Copyright terms: Public domain W3C validator