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 1533 | . 2 ⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒))) | |
2 | had0 1534 | . 2 ⊢ (¬ 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒))) | |
3 | 1, 2 | casesifp 1020 | 1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 if-wif 1006 ⊻ wxo 1456 haddwhad 1523 |
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 196 df-or 384 df-an 385 df-ifp 1007 df-xor 1457 df-had 1524 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |