Theorem xorbi12i

Equality property for exclusive disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)

Hypotheses
xorbi12.1
\( \vdash \varphi \leftrightarrow \psi \)
xorbi12.2
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \veebar \chi \leftrightarrow \psi \veebar \theta \)
Proof
l0
df-xor
\( \vdash \varphi \veebar \chi \leftrightarrow \neg (\varphi \leftrightarrow \chi) \)
l1
xorbi12.1
xorbi12.2
bibi12i l1 _
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow \theta) \)
l4
xchbinx l0 _
\( \vdash \varphi \veebar \chi \leftrightarrow \neg (\psi \leftrightarrow \theta) \)
df-xor
\( \vdash \psi \veebar \theta \leftrightarrow \neg (\psi \leftrightarrow \theta) \)
bitr4i l4 _