Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cadifp | Structured version Visualization version GIF version |
Description: The value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs. (Contributed by BJ, 8-Oct-2019.) |
Ref | Expression |
---|---|
cadifp | ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cad1 1616 | . 2 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) | |
2 | cad0 1617 | . 2 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | casesifp 1071 | 1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∨ wo 843 if-wif 1057 caddwcad 1606 |
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 209 df-an 399 df-or 844 df-ifp 1058 df-3or 1084 df-3an 1085 df-xor 1502 df-cad 1607 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |