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 34701
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 34700 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1087 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 395 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 206 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  34714  bnj250  34715  bnj258  34722  bnj268  34723  bnj291  34725  bnj312  34726  bnj446  34731  bnj645  34764  bnj658  34765  bnj887  34779  bnj919  34781  bnj945  34787  bnj951  34789  bnj982  34792  bnj1019  34793  bnj518  34900  bnj571  34920  bnj594  34926  bnj916  34947  bnj966  34958  bnj967  34959  bnj1006  34974  bnj1018g  34977  bnj1018  34978  bnj1040  34986  bnj1174  35017  bnj1175  35018  bnj1311  35038
  Copyright terms: Public domain W3C validator