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

Theorem hadifp 1584
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 1582 . 2 (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓𝜒)))
2 had0 1583 . 2 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓𝜒)))
31, 2casesifp 1046 1 (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓𝜒), (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  if-wif 1032  wxo 1504  haddwhad 1572
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-or 384  df-an 385  df-ifp 1033  df-xor 1505  df-had 1573
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator