Where does this rule for Boolean simplification come from? In the simplification:
$$\begin{align}A'BC + AB'C + ABC \\
BC(A' + A) + AB'C \\
BC + AB'C \\
\color{red}{C(B + AB')} \\
\color{blue}{C(B + A)} \\
AC + BC\end{align}$$
What is the rule that permits going from the red step to blue step? It doesn't immediately jump out at me as an obvious next step. Normally with these Boolean simplifications you can treat them like normal arithmetic but then I don't see which rule applies.
 A: When you read $B+AB'$ as "$B$ or ($A$ and not $B$)" then it should become obvious that it means that it is $B$ or (it is not and) it is $A$; that is is "$B$ or $A$". 
To spell it out in three simple steps:
$$\begin{split}B+A\cdot B' &= (B+A)\cdot (B+B')\quad&\text{distribution} \\&= (B+A)\cdot 1&\text{complementation}\\&=B+A&\text{conjunctive identity}\end{split}$$
A: $$
\begin{align*}
B + A B' &= (A+A')B + AB' && A + A' = 1\\
&= AB + A'B + AB' && \text{distributivity}\\
&= AB + AB+ A'B + AB' && \text{absorption}\\
&= A(B+ B') + AB + A'B && \text{distributivity} \\
&= A + (A + A')B && B + B' = 1 \wedge \text{ distributivity}\\
&= A + B && A + A' = 1 \\
&= B + A && \text{commutativity}
\end{align*}
$$

edit: I'll try to explain how I almost instantly saw that $B + AB' = B+A$ is true and how this informed my verification above.
Let $X$ be a set. There is a very natural Boolean algebra associated to $X$, namely $\mathcal{B}_X = (B_X; +, \cdot, ', 0, 1)$ with


*

*$B_X := \mathcal{P}(X)$ (the set of all subsets of $X$),

*$a + b := a \cup b$,

*$a \cdot b := a \cap b$,

*$a' := X \setminus a$,

*$0 := \emptyset$ and

*$1 := X$.


In this Boolean algebra we have
$$
B + AB' = B + A \iff B \cup (A \cap X \setminus B) = B \cup A.
$$
Anyone familiar with elementary set theory will intuitively know (and be able to easily verify) that the latter equality is true. So the former equality is true in $\mathcal{B}_X$ for all sets $X$.
One very useful fact about Boolean algebras is that for every Boolean algebra $B$ there is some set $X$ such that $\mathcal{B}_X$ contains a copy of $B$ (i.e. there is a monomorphism $B \to \mathcal{B}_X$). This immediately implies that it suffices to verify $B + AB' = B+A$ only for the special sorts of Boolean algebras $\mathcal{B}_{X}$ for all $X$ to conclude that it must hold in all Boolean algebras.
Once I knew that, I again worked inside of $\mathcal{B}_{X}$ to construct the above computation that formally proves the equality $B \cup (A \cap X \setminus B) = B \cup A$ in the language of Boolean algebras. Finally, I translated the rules of elementary set manipulation to the corresponding rules for Boolean algebras to justify my manipulations.
A: This equivalence is common enough that it has a name:
Reduction
$P+P'Q=P+Q$
A: The rule is the following 'generalized reduction' rule:$$
P + (\ldots P \ldots) = P + (\ldots 0 \ldots)
$$ In words: on one side of an 'or' / disjunction / $\;+\;$ you may assume that the other side is false / $\;0\;$.  So $\;B+A\cdot B' = B+A\cdot 0'\;$, which quickly simplifies to $\;B + A\;$.

Note that dually, $$
P \cdot (\ldots P \ldots) = P \cdot (\ldots 1 \ldots)
$$  In words: on one side of an 'and' / conjunction / $\;\cdot\;$ you may assume that the other side is true /$\;1\;$.

A very simple 'semantical' proof for the first rule is: If $\;P=1\;$ then both sides of the above equality simplify to $\;1\;$, and if $\;P=0\;$ then both sides become $\;(\ldots 0 \ldots)\;$.
(See this comment, thanks to Fabio Somenzi, in response to my follow-up question: What is the "official" name for these boolean algebra rules?)

A 'structural' systematic (inductive) way to prove this rule, is to use the usual reduction rule $\;P + Q = P + P' \cdot Q\;$, and then distribute $\;P'\cdot{}\;$ inward, towards each occurrence of $\;P\;$.  In this specific case, that leads to the calculation $$B+A\cdot B' = B + B' \cdot A \cdot B' = B + A \cdot (B' \cdot B') = A \cdot (B + B)' = A \cdot (B + 0)'$$  Then working outward again, we get $$ {} = A \cdot B' \cdot 0' = B' \cdot A \cdot 0' = A \cdot 0'$$
This inductive proof ultimately relies on the fact that $\;P' \cdot P = P' \cdot 0\;$ and $\;P + P = P + 0\;$.
