Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical equivalence
wb
Next ⟩
df-bi
Metamath Proof Explorer
Unicode
Structured
Syntax definition
wb
Description:
Extend wff definition to include the biconditional connective.
Ref
Expression
Assertion
wb
wff ( ph <-> ps )