|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > hadifp | Structured version Visualization version GIF version | ||
| Description: The value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs. (Contributed by BJ, 11-Aug-2020.) | 
| Ref | Expression | 
|---|---|
| hadifp | ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | had1 1603 | . 2 ⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒))) | |
| 2 | had0 1604 | . 2 ⊢ (¬ 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒))) | |
| 3 | 1, 2 | casesifp 1078 | 1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 if-wif 1063 ⊻ wxo 1511 haddwhad 1593 | 
| 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 849 df-ifp 1064 df-xor 1512 df-had 1594 | 
| This theorem is referenced by: wl-df-3xor 37469 | 
| Copyright terms: Public domain | W3C validator |