Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical equivalence
wb
Next ⟩
df-bi
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
wb
Description:
Extend wff definition to include the biconditional connective.
Ref
Expression
Assertion
wb
$${wff}\left({\phi}\leftrightarrow {\psi}\right)$$