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 30881
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 30880 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1054 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 383 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 196 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  30894  bnj250  30895  bnj258  30902  bnj268  30903  bnj291  30905  bnj312  30906  bnj446  30911  bnj645  30946  bnj658  30947  bnj887  30961  bnj919  30963  bnj945  30970  bnj951  30972  bnj982  30975  bnj1019  30976  bnj518  31082  bnj571  31102  bnj594  31108  bnj916  31129  bnj966  31140  bnj967  31141  bnj1006  31155  bnj1018  31158  bnj1040  31166  bnj1174  31197  bnj1175  31198  bnj1311  31218
  Copyright terms: Public domain W3C validator