Theorem hadifp 1636

Description: The value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs. (Contributed by BJ, 11-Aug-2020.)

Assertion

Ref	Expression
hadifp	⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))

Proof of Theorem hadifp

Step	Hyp	Ref	Expression
1		had1 1632	. . 3 ⊢ (𝜑 ↔ (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒)))
2	1	biimpi 219	. 2 ⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒)))
3		had0 1633	. . 3 ⊢ (¬ 𝜑 ↔ (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒)))
4	3	biimpi 219	. 2 ⊢ (¬ 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒)))
5	2, 4	casesifp 1094	1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  if-wif 1078   ⊻ wxo 1540  haddwhad 1622

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079  df-xor 1541  df-had 1623

This theorem is used by:  wl-df-3xor  38467