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 30006
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 30005 . 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  30019  bnj250  30020  bnj258  30027  bnj268  30028  bnj291  30030  bnj312  30031  bnj446  30036  bnj645  30074  bnj658  30075  bnj887  30089  bnj919  30091  bnj945  30098  bnj951  30100  bnj982  30103  bnj1019  30104  bnj518  30210  bnj571  30230  bnj594  30236  bnj916  30257  bnj966  30268  bnj967  30269  bnj1006  30283  bnj1018  30286  bnj1040  30294  bnj1174  30325  bnj1175  30326  bnj1311  30346
  Copyright terms: Public domain W3C validator