Theorem wl-df-had 34761

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

Check whether an odd number of three inputs are true. The ⊻ operation tests this for two inputs, 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 to an odd number.

If the inputs are viewed as binary digits (true is 1, false is 0), the result is what a binary full addition leaves in the lowest bit of their sum. That is what the name "had" is derived from: "half adder". (Contributed by Wolf Lammen, 24-Apr-2024.)

Assertion

Ref	Expression
wl-df-had	⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))

Proof of Theorem wl-df-had

Step	Hyp	Ref	Expression
1		hadifp 1606	1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))

Syntax hints:   ↔ wb 208  if-wif 1057   ⊻ wxo 1501  haddwhad 1593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ifp 1058  df-xor 1502  df-had 1594

This theorem is referenced by:  wl-had1  34762  wl-had0  34763  wl-dfhad2  34764