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 (φ, ψ, χ) \leftrightarrow ((φ \to ψ) \land ((φ \land χ) \leftrightarrow (ψ \land χ)))$

Step	Hyp	Ref	Expression
0		wph	$wff φ$
1		wps	$wff ψ$
2		wch	$wff χ$
3	0 1 2	wredundp	$wff redund (φ, ψ, χ)$
4	0 1	wi	$wff (φ \to ψ)$
5	0 2	wa	$wff (φ \land χ)$
6	1 2	wa	$wff (ψ \land χ)$
7	5 6	wb	$wff ((φ \land χ) \leftrightarrow (ψ \land χ))$
8	4 7	wa	$wff ((φ \to ψ) \land ((φ \land χ) \leftrightarrow (ψ \land χ)))$
9	3 8	wb	$wff (redund (φ, ψ, χ) \leftrightarrow ((φ \to ψ) \land ((φ \land χ) \leftrightarrow (ψ \land χ))))$

Metamath Proof Explorer