Metamath Proof Explorer


Syntax definition wredundp

Description: Extend wff definition to include the redundancy operator for propositions.

Ref Expression
Assertion wredundp wff redund φ ψ χ