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 31077
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 31076 . 2 wff (𝜑𝜓𝜒𝜃)
61, 2, 3w3a 1100 . . 3 wff (𝜑𝜓𝜒)
76, 4wa 384 . 2 wff ((𝜑𝜓𝜒) ∧ 𝜃)
85, 7wb 197 1 wff ((𝜑𝜓𝜒𝜃) ↔ ((𝜑𝜓𝜒) ∧ 𝜃))
Colors of variables: wff setvar class
This definition is referenced by:  bnj248  31090  bnj250  31091  bnj258  31098  bnj268  31099  bnj291  31101  bnj312  31102  bnj446  31107  bnj645  31141  bnj658  31142  bnj887  31156  bnj919  31158  bnj945  31165  bnj951  31167  bnj982  31170  bnj1019  31171  bnj518  31277  bnj571  31297  bnj594  31303  bnj916  31324  bnj966  31335  bnj967  31336  bnj1006  31350  bnj1018  31353  bnj1040  31361  bnj1174  31392  bnj1175  31393  bnj1311  31413
  Copyright terms: Public domain W3C validator