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 29800
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 29799 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1031 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 383 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 195 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  29813  bnj250  29814  bnj258  29821  bnj268  29822  bnj291  29824  bnj312  29825  bnj446  29830  bnj645  29868  bnj658  29869  bnj887  29883  bnj919  29885  bnj945  29892  bnj951  29894  bnj982  29897  bnj1019  29898  bnj518  30004  bnj571  30024  bnj594  30030  bnj916  30051  bnj966  30062  bnj967  30063  bnj1006  30077  bnj1018  30080  bnj1040  30088  bnj1174  30119  bnj1175  30120  bnj1311  30140
  Copyright terms: Public domain W3C validator