Metamath Proof Explorer


Theorem wl-3xorrot

Description: Rotation law for triple xor. (Contributed by Mario Carneiro, 4-Sep-2016) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024)

Ref Expression
Assertion wl-3xorrot hadd φ ψ χ hadd ψ χ φ

Proof

Step Hyp Ref Expression
1 bicom φ ψ χ ψ χ φ
2 wl-3xorbi hadd φ ψ χ φ ψ χ
3 wl-3xorbi2 hadd ψ χ φ ψ χ φ
4 1 2 3 3bitr4i hadd φ ψ χ hadd ψ χ φ