Metamath Proof Explorer


Theorem wl-3xornot

Description: Triple xor distributes over negation. Copy of hadnot . (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

Ref Expression
Assertion wl-3xornot ( ¬ hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ hadd ( ¬ 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 notbi ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
2 1 bibi1i ( ( ( 𝜑𝜓 ) ↔ ¬ 𝜒 ) ↔ ( ( ¬ 𝜑 ↔ ¬ 𝜓 ) ↔ ¬ 𝜒 ) )
3 xor3 ( ¬ ( ( 𝜑𝜓 ) ↔ 𝜒 ) ↔ ( ( 𝜑𝜓 ) ↔ ¬ 𝜒 ) )
4 wl-3xorbi2 ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑𝜓 ) ↔ 𝜒 ) )
5 3 4 xchnxbir ( ¬ hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑𝜓 ) ↔ ¬ 𝜒 ) )
6 wl-3xorbi2 ( hadd ( ¬ 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) ↔ ( ( ¬ 𝜑 ↔ ¬ 𝜓 ) ↔ ¬ 𝜒 ) )
7 2 5 6 3bitr4i ( ¬ hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ hadd ( ¬ 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) )