Metamath Proof Explorer


Syntax definition wif

Description: Extend wff notation to include the conditional operator for propositions.

Ref Expression
Assertion wif wffif-φψχ