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 1546 | . 2 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) | |
2 | cad0 1547 | . 2 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | casesifp 1020 | 1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∨ wo 382 ∧ wa 383 if-wif 1006 caddwcad 1536 |
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-3or 1032 df-3an 1033 df-xor 1457 df-cad 1537 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |