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