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 ( 𝜒 , 𝜏 , 𝜁 ) ) )