|   | 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 1077 | 1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∨ wo 847 if-wif 1062 caddwcad 1605 | 
| 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 207 df-an 396 df-or 848 df-ifp 1063 df-3or 1087 df-3an 1088 df-xor 1511 df-cad 1606 | 
| This theorem is referenced by: wl-df-3mintru2 37486 | 
| Copyright terms: Public domain | W3C validator |