Metamath Proof Explorer


Theorem wl-3xorbi2

Description: Alternative form of wl-3xorbi . (Contributed by Mario Carneiro, 4-Sep-2016) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024)

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

Proof

Step Hyp Ref Expression
1 wl-3xorbi haddφψχφψχ
2 biass φψχφψχ
3 1 2 bitr4i haddφψχφψχ