Metamath Proof Explorer


Theorem wl-3xorbi123i

Description: Equivalence theorem for triple xor. Copy of hadbi123i . (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Hypotheses wl-3xorbii.1 ψ χ
wl-3xorbii.2 θ τ
wl-3xorbii.3 η ζ
Assertion wl-3xorbi123i hadd ψ θ η hadd χ τ ζ

Proof

Step Hyp Ref Expression
1 wl-3xorbii.1 ψ χ
2 wl-3xorbii.2 θ τ
3 wl-3xorbii.3 η ζ
4 1 a1i ψ χ
5 2 a1i θ τ
6 3 a1i η ζ
7 4 5 6 wl-3xorbi123d hadd ψ θ η hadd χ τ ζ
8 7 mptru hadd ψ θ η hadd χ τ ζ