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 34879
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 34878 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1092 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 396 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 207 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  34892  bnj250  34893  bnj258  34900  bnj268  34901  bnj291  34903  bnj312  34904  bnj446  34909  bnj645  34942  bnj658  34943  bnj887  34957  bnj919  34959  bnj945  34965  bnj951  34967  bnj982  34970  bnj1019  34971  bnj518  35077  bnj571  35097  bnj594  35103  bnj916  35124  bnj966  35135  bnj967  35136  bnj1006  35151  bnj1018g  35154  bnj1018  35155  bnj1040  35163  bnj1174  35194  bnj1175  35195  bnj1311  35215
  Copyright terms: Public domain W3C validator