Theorem xorbi12d

Equality property for exclusive disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)

Hypotheses
xor12d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
xor12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \veebar \theta \leftrightarrow \chi \veebar \tau) \)
Proof
l0
xor12d.1
xor12d.2
bibi12d l0 _
l3
notbid _
\( \vdash \varphi \rightarrow (\neg (\psi \leftrightarrow \theta) \leftrightarrow \neg (\chi \leftrightarrow \tau)) \)
l4
df-xor
\( \vdash \psi \veebar \theta \leftrightarrow \neg (\psi \leftrightarrow \theta) \)
df-xor
\( \vdash \chi \veebar \tau \leftrightarrow \neg (\chi \leftrightarrow \tau) \)
3bitr4g l3 l4 _