Metamath Proof Explorer


Syntax definition wif

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

Ref Expression
Assertion wif wff if- ( 𝜑 , 𝜓 , 𝜒 )