Metamath Proof Explorer

Theorem wl-3xorbi123d

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

Ref Expression
Hypotheses wl-3xorbid.1 ⊢ φ → ψ ↔ χ
wl-3xorbid.2 ⊢ φ → θ ↔ τ
wl-3xorbid.3 ⊢ φ → η ↔ ζ
Assertion wl-3xorbi123d ⊢ φ → hadd ψ θ η ↔ hadd χ τ ζ

Proof

Step Hyp Ref Expression
1 wl-3xorbid.1 ⊢ φ → ψ ↔ χ
2 wl-3xorbid.2 ⊢ φ → θ ↔ τ
3 wl-3xorbid.3 ⊢ φ → η ↔ ζ
4 1 2 bibi12d ⊢ φ → ψ ↔ θ ↔ χ ↔ τ
5 4 3 bibi12d ⊢ φ → ψ ↔ θ ↔ η ↔ χ ↔ τ ↔ ζ
6 wl-3xorbi2 ⊢ hadd ψ θ η ↔ ψ ↔ θ ↔ η
7 wl-3xorbi2 ⊢ hadd χ τ ζ ↔ χ ↔ τ ↔ ζ
8 5 6 7 3bitr4g ⊢ φ → hadd ψ θ η ↔ hadd χ τ ζ