Theorem wl-df-had

Description: Alternative definition of whad based on hadifp . See df-had to learn how it is currently introduced.

Check whether an odd number of inputs are true. The oddness of two is expressed by the \/_ operation, and for evenness we can use <-> . So, if the first input is true, the two remaining inputs need to amount to an even number, else an odd number is required. (Contributed by Wolf Lammen, 24-Apr-2024)

	Ref	Expression
Assertion	wl-df-had	$$⊢hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow if-\left(\phi ,\left(\psi \leftrightarrow \chi \right),\left(\psi ⊻\chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hadifp	$$⊢hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow if-\left(\phi ,\left(\psi \leftrightarrow \chi \right),\left(\psi ⊻\chi \right)\right)$$