Theorem hadcomaOLD

Description: Obsolete version of hadcoma as of 17-Dec-2023. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hadcomaOLD	$$⊢hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow hadd\left(\psi ,\phi ,\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		xorcom	$$⊢\left(\phi ⊻\psi \right)\leftrightarrow \left(\psi ⊻\phi \right)$$
2		biid	$$⊢\chi \leftrightarrow \chi$$
3	1 2	xorbi12i	$$⊢\left(\left(\phi ⊻\psi \right)⊻\chi \right)\leftrightarrow \left(\left(\psi ⊻\phi \right)⊻\chi \right)$$
4		df-had	$$⊢hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\left(\phi ⊻\psi \right)⊻\chi \right)$$
5		df-had	$$⊢hadd\left(\psi ,\phi ,\chi \right)\leftrightarrow \left(\left(\psi ⊻\phi \right)⊻\chi \right)$$
6	3 4 5	3bitr4i	$$⊢hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow hadd\left(\psi ,\phi ,\chi \right)$$