Definition df-redundp 38648

Description: Define the redundancy operator for propositions, cf. df-redund 38647. (Contributed by Peter Mazsa, 23-Oct-2022.)

Assertion

Ref	Expression
df-redundp	⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))))

Detailed syntax breakdown of Definition df-redundp

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	wredundp 38226	. 2 wff redund (𝜑, 𝜓, 𝜒)
5	1, 2	wi 4	. . 3 wff (𝜑 → 𝜓)
6	1, 3	wa 395	. . . 4 wff (𝜑 ∧ 𝜒)
7	2, 3	wa 395	. . . 4 wff (𝜓 ∧ 𝜒)
8	6, 7	wb 206	. . 3 wff ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
9	5, 8	wa 395	. 2 wff ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))
10	4, 9	wb 206	1 wff ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))))

This definition is referenced by:  redundpim3  38653  redundpbi1  38654  refrelredund4  38658