Theorem hadifp 1637

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 1633	. . 3 ⊢ (𝜑 ↔ (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒)))
2	1	biimpi 219	. 2 ⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒)))
3		had0 1634	. . 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 1541  haddwhad 1623

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 1542  df-had 1624

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