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 1623 | . 2 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) | |
2 | cad0 1624 | . 2 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | casesifp 1076 | 1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∨ wo 844 if-wif 1060 caddwcad 1612 |
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 397 df-or 845 df-ifp 1061 df-3or 1087 df-3an 1088 df-xor 1507 df-cad 1613 |
This theorem is referenced by: wl-df-3mintru2 35643 |
Copyright terms: Public domain | W3C validator |