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

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
StepHypRef Expression
1 had1 1603 . 2 (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓𝜒)))
2 had0 1604 . 2 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓𝜒)))
31, 2casesifp 1078 1 (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓𝜒), (𝜓𝜒)))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator