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 ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> ch ) )

Proof

Step Hyp Ref Expression
1 wl-3xorbi 
 |-  ( hadd ( ph , ps , ch ) <-> ( ph <-> ( ps <-> ch ) ) )
2 biass 
 |-  ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) )
3 1 2 bitr4i 
 |-  ( hadd ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> ch ) )