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 31033
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 31032 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1072 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 383 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 196 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  31046  bnj250  31047  bnj258  31054  bnj268  31055  bnj291  31057  bnj312  31058  bnj446  31063  bnj645  31098  bnj658  31099  bnj887  31113  bnj919  31115  bnj945  31122  bnj951  31124  bnj982  31127  bnj1019  31128  bnj518  31234  bnj571  31254  bnj594  31260  bnj916  31281  bnj966  31292  bnj967  31293  bnj1006  31307  bnj1018  31310  bnj1040  31318  bnj1174  31349  bnj1175  31350  bnj1311  31370
  Copyright terms: Public domain W3C validator