NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-cad Unicode 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
2 wps . . 3
3 wch . . 3
41, 2, 3wcad 1379 . 2 cadd
51, 2wa 358 . . 3
61, 2wxo 1304 . . . 4  \/_
73, 6wa 358 . . 3  \/_
85, 7wo 357 . 2  \/_
94, 8wb 176 1 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