Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > hadifp | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
hadifp | ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | had1 1542 | . 2 ⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒))) | |
2 | had0 1543 | . 2 ⊢ (¬ 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒))) | |
3 | 1, 2 | casesifp 1026 | 1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 if-wif 1012 ⊻ wxo 1464 haddwhad 1532 |
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 385 df-an 386 df-ifp 1013 df-xor 1465 df-had 1533 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |