👮‍♂️ Proof by case distinction §

= If the assumption from A leads us to B, and if the assumption from ¬A also leads us to B, then we may infer B, and the assumptions A and ¬A can both be eliminated.

Notation §

(FU) \frac{\begin{array} & {[A]_{i}} \\ \vdots \\ B \end{array} \quad \begin{array} & {[\neg A]_{i}} \\ \vdots \\ B \end{array}}{B}i