Metamath Proof Explorer


Theorem wl-3xorfal

Description: If the first input is false, then triple xor is equivalent to the exclusive disjunction of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016) df-had redefined. (Revised by Wolf Lammen, 29-Apr-2024)

Ref Expression
Assertion wl-3xorfal
|- ( -. ph -> ( hadd ( ph , ps , ch ) <-> ( ps \/_ ch ) ) )

Proof

Step Hyp Ref Expression
1 wl-df-3xor
 |-  ( hadd ( ph , ps , ch ) <-> if- ( ph , -. ( ps \/_ ch ) , ( ps \/_ ch ) ) )
2 ifpfal
 |-  ( -. ph -> ( if- ( ph , -. ( ps \/_ ch ) , ( ps \/_ ch ) ) <-> ( ps \/_ ch ) ) )
3 1 2 syl5bb
 |-  ( -. ph -> ( hadd ( ph , ps , ch ) <-> ( ps \/_ ch ) ) )