Laws of Boolean algebra: every law with a proof and examples

Every law of Boolean algebra the engine applies, each stated in four notations and proved on every row of its truth table.

The 29 laws below are the exact rewriting rules the Tangibool simplifier, normal-form converter and gate-basis transformer use, named as the engine names them (and as textbooks name them where the two differ: the null law is the engine's domination law, involution is double negation). Three more, the commutative law, the consensus theorem and Huntington's postulates, are stated here because they are what students look up, and the engine proves them the same way.

A law page gives the statement in words, programming, mathematical and algebra notation, the truth table with both sides as columns, the checker's verdict over every assignment, a gate diagram of each side, the slip people make with that law, the lesson that teaches it, and the worked examples whose simplification used it.

If you want to see a law at work on your own expression, the simplifier names the law at each step and verifies that the step kept the function unchanged.

• Identity law of Boolean algebra: A AND TRUE = A, A OR FALSE = A
  The identity law says that combining a value with the neutral constant leaves it unchanged: TRUE is neutral for AND and FALSE is neutral for OR.
• Null law (domination): A AND FALSE = FALSE, A OR TRUE = TRUE
  The null law (the engine calls it domination) says that the dominant constant fixes the result whatever the other operand is: FALSE dominates AND and TRUE dominates OR.
• Idempotent law: A AND A = A, A OR A = A
  The idempotent law says that combining a value with itself by AND or by OR gives the value back: A AND A = A and A OR A = A.
• Complement law: A AND NOT A = FALSE, A OR NOT A = TRUE
  The complement law says that a value combined with its own negation gives FALSE under AND and TRUE under OR: A AND NOT A = FALSE, A OR NOT A = TRUE.
• Absorption law: A OR (A AND B) = A, with proof
  The absorption law says that a value absorbs any term that contains it: A OR (A AND B) = A and A AND (A OR B) = A.
• Double negation (involution): NOT NOT A = A
  Double negation (also called involution) says that negating a value twice gives back the original: NOT NOT A = A.
• De Morgan's laws: NOT (A AND B) = NOT A OR NOT B, with proof and examples
  De Morgan's laws say how a negation passes through AND and OR: the negation of an AND is the OR of the negations, and the negation of an OR is the AND of the negations.
• Negating constants: NOT TRUE = FALSE, NOT FALSE = TRUE
  Negating a constant gives the other constant: NOT TRUE = FALSE and NOT FALSE = TRUE.
• XOR identities: A XOR FALSE = A, A XOR TRUE = NOT A, A XOR A = FALSE
  The XOR identities: XOR with FALSE leaves a value unchanged, XOR with TRUE negates it, and a value XOR itself is FALSE.
• Associative law: (A AND B) AND C = A AND (B AND C)
  The associative law says that regrouping a chain of the same operator does not change its value: (A AND B) AND C = A AND (B AND C), and likewise for OR and XOR.
• Implication elimination: A → B = NOT A OR B, and the →E rule
  Implication elimination rewrites A -> B as NOT A OR B: an implication is true unless its condition holds and its consequence fails.
• Biconditional elimination: the A ↔ B rewrite and the ↔E rule
  Biconditional elimination rewrites A <-> B as (A AND B) OR (NOT A AND NOT B): both true, or both false.
• XOR elimination: A XOR B = (A AND NOT B) OR (NOT A AND B)
  XOR elimination rewrites A XOR B as (A AND NOT B) OR (NOT A AND B): the first true and the second false, or the other way round.
• NAND elimination: NAND(A, B) = NOT (A AND B)
  NAND elimination rewrites NAND(A, B) as NOT (A AND B): a NAND is an AND followed by a NOT.
• NOR elimination: NOR(A, B) = NOT (A OR B)
  NOR elimination rewrites NOR(A, B) as NOT (A OR B): a NOR is an OR followed by a NOT, true only when both inputs are false.
• XNOR elimination: XNOR(A, B) = A ↔ B
  XNOR elimination rewrites XNOR(A, B) as the biconditional A <-> B: the gate that is true when both inputs are equal is the connective that says “if and only if”.
• Distributive law: A AND (B OR C) = (A AND B) OR (A AND C), both forms
  The distributive law says that AND distributes over OR and OR distributes over AND: A AND (B OR C) = (A AND B) OR (A AND C) and A OR (B AND C) = (A OR B) AND (A OR C).
• Minterm expansion: the canonical sum of products (Σm)
  Minterm expansion rewrites a formula as the OR of one AND term per truth-table row where it is true: the canonical sum of products, written Σm(…).
• Maxterm expansion: the canonical product of sums (ΠM)
  Maxterm expansion rewrites a formula as the AND of one OR term per truth-table row where it is false: the canonical product of sums, written ΠM(…).
• Subcircuit expansion (Tangibool rewriting step)
  Subcircuit expansion replaces an instance of a reusable subcircuit by its definition body, with the instance's arguments wired to the definition's inputs.in progress
• Named-output reference expansion (Tangibool rewriting step)
  Reference expansion replaces a named output used inside another formula by its definition, so eligible AND C with eligible := A OR B becomes (A OR B) AND C.in progress
• Counting-constraint expansion: AT_LEAST(2; A, B, C) = (A AND B) OR (A AND C) OR (B AND C)
  Counting-constraint expansion rewrites ATLEAST(k; …), ATMOST(k; …) and EXACTLY(k; …) over their operands with AND, OR and NOT, so that normal forms, Karnaugh maps and gate bases can work on a plain…
• NOT from NAND: NOT A = NAND(A, A)
  NOT from NAND: an inverter is a NAND gate with both inputs fed the same signal, NOT A = NAND(A, A).
• AND from NAND gates: A AND B = NAND(NAND(A, B), NAND(A, B))
  AND from NAND gates: A AND B = NAND(NAND(A, B), NAND(A, B)), a NAND followed by a NAND inverter.
• OR from NAND gates: A OR B = NAND(NAND(A, A), NAND(B, B))
  OR from NAND gates: A OR B = NAND(NAND(A, A), NAND(B, B)), a NAND of the two inverted inputs.
• NOT from NOR: NOT A = NOR(A, A)
  NOT from NOR: an inverter is a NOR gate with both inputs tied together, NOT A = NOR(A, A).
• OR from NOR gates: A OR B = NOR(NOR(A, B), NOR(A, B))
  OR from NOR gates: A OR B = NOR(NOR(A, B), NOR(A, B)), a NOR followed by a NOR inverter.
• AND from NOR gates: A AND B = NOR(NOR(A, A), NOR(B, B))
  AND from NOR gates: A AND B = NOR(NOR(A, A), NOR(B, B)), a NOR of the two inverted inputs.
• Karnaugh map grouping rule: adjacent cells drop the variable that changes
  The Karnaugh map grouping rule: adjacent cells with the same value combine into one term that omits the variable changing between them, (A AND B) OR (A AND NOT B) = A.
• Commutative law: A AND B = B AND A, A OR B = B OR A
  The commutative law says that the order of the operands does not matter: A AND B = B AND A, A OR B = B OR A, and the same for XOR.
• Consensus theorem: AB + A'C + BC = AB + A'C, with proof
  The consensus theorem says that the consensus term of two terms is redundant: (A AND B) OR (NOT A AND C) OR (B AND C) = (A AND B) OR (NOT A AND C).
• Huntington's postulates of Boolean algebra, with their duals
  Huntington's postulates are the small set of axioms from which every other law of Boolean algebra follows: closure, the identity elements, commutativity, distributivity in both directions, the…

Questions

Why are there more laws here than in my textbook?

Textbooks list the identities students memorise (identity, null, idempotent, complement, absorption, commutative, associative, distributive, De Morgan, involution). The engine also needs the elimination rules that turn implication, biconditional, XOR, NAND, NOR and XNOR into AND, OR and NOT, the minterm and maxterm expansions, and the NAND-only and NOR-only constructions. They are all laws in the same sense: an identity that holds for every assignment.

Does the order of the laws matter when simplifying?

The simplifier applies laws by a size measure (fewer operators, then fewer literals), not by a fixed order, and stops when no law shortens the expression further. That is why its result is labelled simplified rather than minimal: a different order can reach a shorter form, and the engine never claims that a form is the smallest; the Karnaugh map derives an irreducible cover for up to four variables and checks it on every row.

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.