Theorem xorcom 1366

Description: \/_ is commutative. (Contributed by Mario Carneiro, 4-Sep-2016.)

Assertion

Ref	Expression
xorcom

Proof of Theorem xorcom

Step	Hyp	Ref	Expression
1		bicom 200	. . 3
2	1	notbii 296	. 2
3		df-xor 1364	. 2
4		df-xor 1364	. 2
5	2, 3, 4	3bitr4i 277	1

Syntax hints:  -.wn 3  <->wb 184  \/_wxo 1363

This theorem is referenced by:  xorneg2  1374  hadcoma  1455  hadcomb  1456  cadcoma  1462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-xor 1364