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 ¬ φ hadd φ ψ χ ψ χ

Proof

Step Hyp Ref Expression
1 wl-df-3xor hadd φ ψ χ if- φ ¬ ψ χ ψ χ
2 ifpfal ¬ φ if- φ ¬ ψ χ ψ χ ψ χ
3 1 2 syl5bb ¬ φ hadd φ ψ χ ψ χ