Theorem excluded_middle ≪ | index | src | ≫

排中律

theorem excluded_middle (A: wff): $ A \or \neg A $;
StepHypRefExpression
1 imp_refl 
\neg A \imp \neg A
2 1 conv or 
A \or \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2)