Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-redundp Structured version   Visualization version   GIF version

Definition df-redundp 35925
Description: Define the redundancy operator for propositions, cf. df-redund 35924. (Contributed by Peter Mazsa, 23-Oct-2022.)
Assertion
Ref Expression
df-redundp ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ ((𝜑𝜒) ↔ (𝜓𝜒))))

Detailed syntax breakdown of Definition df-redundp
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
41, 2, 3wredundp 35540 . 2 wff redund (𝜑, 𝜓, 𝜒)
51, 2wi 4 . . 3 wff (𝜑𝜓)
61, 3wa 399 . . . 4 wff (𝜑𝜒)
72, 3wa 399 . . . 4 wff (𝜓𝜒)
86, 7wb 209 . . 3 wff ((𝜑𝜒) ↔ (𝜓𝜒))
95, 8wa 399 . 2 wff ((𝜑𝜓) ∧ ((𝜑𝜒) ↔ (𝜓𝜒)))
104, 9wb 209 1 wff ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ ((𝜑𝜒) ↔ (𝜓𝜒))))
Colors of variables: wff setvar class
This definition is referenced by:  redundpim3  35930  redundpbi1  35931  refrelredund4  35935
  Copyright terms: Public domain W3C validator