NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  cad1 GIF version

Theorem cad1 1398
Description: If one parameter is true, the adder carry is true exactly when at least one of the other parameters is true. (Contributed by Mario Carneiro, 8-Sep-2016.)
Assertion
Ref Expression
cad1 (χ → (cadd(φ, ψ, χ) ↔ (φ ψ)))

Proof of Theorem cad1
StepHypRef Expression
1 ibar 490 . . . 4 (χ → ((φψ) ↔ (χ (φψ))))
21bicomd 192 . . 3 (χ → ((χ (φψ)) ↔ (φψ)))
32orbi2d 682 . 2 (χ → (((φ ψ) (χ (φψ))) ↔ ((φ ψ) (φψ))))
4 df-cad 1381 . 2 (cadd(φ, ψ, χ) ↔ ((φ ψ) (χ (φψ))))
5 pm5.63 890 . . 3 (((φ ψ) (φ ψ)) ↔ ((φ ψ) (¬ (φ ψ) (φ ψ))))
6 olc 373 . . . 4 ((φ ψ) → ((φ ψ) (φ ψ)))
7 orc 374 . . . . . 6 (φ → (φ ψ))
87adantr 451 . . . . 5 ((φ ψ) → (φ ψ))
9 id 19 . . . . 5 ((φ ψ) → (φ ψ))
108, 9jaoi 368 . . . 4 (((φ ψ) (φ ψ)) → (φ ψ))
116, 10impbii 180 . . 3 ((φ ψ) ↔ ((φ ψ) (φ ψ)))
12 xor2 1310 . . . . 5 ((φψ) ↔ ((φ ψ) ¬ (φ ψ)))
13 ancom 437 . . . . 5 (((φ ψ) ¬ (φ ψ)) ↔ (¬ (φ ψ) (φ ψ)))
1412, 13bitri 240 . . . 4 ((φψ) ↔ (¬ (φ ψ) (φ ψ)))
1514orbi2i 505 . . 3 (((φ ψ) (φψ)) ↔ ((φ ψ) (¬ (φ ψ) (φ ψ))))
165, 11, 153bitr4i 268 . 2 ((φ ψ) ↔ ((φ ψ) (φψ)))
173, 4, 163bitr4g 279 1 (χ → (cadd(φ, ψ, χ) ↔ (φ ψ)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358  wxo 1304  caddwcad 1379
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 177  df-or 359  df-an 360  df-xor 1305  df-cad 1381
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator