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

Definition df-cad 1381
Description: Define the half adder carry, which is true when at least two arguments are true. (Contributed by Mario Carneiro, 4-Sep-2016.)
Assertion
Ref Expression
df-cad (cadd(φ, ψ, χ) ↔ ((φ ψ) (χ (φψ))))

Detailed syntax breakdown of Definition df-cad
StepHypRef Expression
1 wph . . 3 wff φ
2 wps . . 3 wff ψ
3 wch . . 3 wff χ
41, 2, 3wcad 1379 . 2 wff cadd(φ, ψ, χ)
51, 2wa 358 . . 3 wff (φ ψ)
61, 2wxo 1304 . . . 4 wff (φψ)
73, 6wa 358 . . 3 wff (χ (φψ))
85, 7wo 357 . 2 wff ((φ ψ) (χ (φψ)))
94, 8wb 176 1 wff (cadd(φ, ψ, χ) ↔ ((φ ψ) (χ (φψ))))
Colors of variables: wff setvar class
This definition is referenced by:  cadbi123d  1383  cador  1391  cadcoma  1395  cad1  1398  cad11  1399  cad0  1400
  Copyright terms: Public domain W3C validator