Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Notations
wredundp
Next ⟩
cdmqss
Metamath Proof Explorer
Ascii
Structured
Syntax definition
wredundp
Description:
Extend wff definition to include the redundancy operator for propositions.
Ref
Expression
Assertion
wredundp
wff
redund (
𝜑
,
𝜓
,
𝜒
)