Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical "xor"
xnor
Next ⟩
xorcom
Metamath Proof Explorer
Ascii
Unicode
Theorem
xnor
Description:
Two ways to write XNOR (exclusive not-or).
(Contributed by
Mario Carneiro
, 4-Sep-2016)
Ref
Expression
Assertion
xnor
⊢
φ
↔
ψ
↔
¬
φ
⊻
ψ
Proof
Step
Hyp
Ref
Expression
1
df-xor
⊢
φ
⊻
ψ
↔
¬
φ
↔
ψ
2
1
con2bii
⊢
φ
↔
ψ
↔
¬
φ
⊻
ψ