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 1555 | . 2 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) | |
2 | cad0 1556 | . 2 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | casesifp 1026 | 1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∨ wo 383 ∧ wa 384 if-wif 1012 caddwcad 1545 |
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-3or 1038 df-3an 1039 df-xor 1465 df-cad 1546 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |