Theorem hadifp 1605

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 1603	. 2 ⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒)))
2		had0 1604	. 2 ⊢ (¬ 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒)))
3	1, 2	casesifp 1078	1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))

Syntax hints:   ↔ wb 206  if-wif 1063   ⊻ wxo 1511  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 207  df-an 396  df-or 849  df-ifp 1064  df-xor 1512  df-had 1594

This theorem is referenced by:  wl-df-3xor  37469