MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hadifp Structured version   Visualization version   GIF version

Theorem hadifp 1691
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
StepHypRef Expression
1 had1 1689 . 2 (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓𝜒)))
2 had0 1690 . 2 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓𝜒)))
31, 2casesifp 1062 1 (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓𝜒), (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  if-wif 1048  wxo 1611  haddwhad 1679
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 197  df-an 383  df-or 827  df-ifp 1049  df-xor 1612  df-had 1680
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator