Definition df-redundp

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	0 1 2	wredundp	⊢ redund ( 𝜑 , 𝜓 , 𝜒 )
4	0 1	wi	⊢ ( 𝜑 → 𝜓 )
5	0 2	wa	⊢ ( 𝜑 ∧ 𝜒 )
6	1 2	wa	⊢ ( 𝜓 ∧ 𝜒 )
7	5 6	wb	⊢ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) )
8	4 7	wa	⊢ ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) )
9	3 8	wb	⊢ ( redund ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ) )