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 34189
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 34188 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1084 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 395 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 205 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  34202  bnj250  34203  bnj258  34210  bnj268  34211  bnj291  34213  bnj312  34214  bnj446  34219  bnj645  34252  bnj658  34253  bnj887  34267  bnj919  34269  bnj945  34275  bnj951  34277  bnj982  34280  bnj1019  34281  bnj518  34388  bnj571  34408  bnj594  34414  bnj916  34435  bnj966  34446  bnj967  34447  bnj1006  34462  bnj1018g  34465  bnj1018  34466  bnj1040  34474  bnj1174  34505  bnj1175  34506  bnj1311  34526
  Copyright terms: Public domain W3C validator