Metamath Proof Explorer

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 wff φ
1 wps wff ψ
2 wch wff χ
3 0 1 2 wredundp wff redund φ ψ χ
4 0 1 wi wff φ → ψ
5 0 2 wa wff φ ∧ χ
6 1 2 wa wff ψ ∧ χ
7 5 6 wb wff φ ∧ χ ↔ ψ ∧ χ
8 4 7 wa wff φ → ψ ∧ φ ∧ χ ↔ ψ ∧ χ
9 3 8 wb wff redund φ ψ χ ↔ φ → ψ ∧ φ ∧ χ ↔ ψ ∧ χ