![]() |
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 1619 | . 2 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) | |
2 | cad0 1620 | . 2 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | casesifp 1078 | 1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∨ wo 846 if-wif 1062 caddwcad 1608 |
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 206 df-an 398 df-or 847 df-ifp 1063 df-3or 1089 df-3an 1090 df-xor 1511 df-cad 1609 |
This theorem is referenced by: wl-df-3mintru2 36365 |
Copyright terms: Public domain | W3C validator |