Metamath Proof Explorer


Syntax definition wb

Description: Extend wff definition to include the biconditional connective.

Ref Expression
Assertion wb wff ( 𝜑𝜓 )