Theorem binary1 ≪ | index | src | ≫

二值遍历式之单个变量

theorem binary1 (A: wff): $ A \or \neg A $;

Step	Hyp	Ref	Expression
1		excluded_middle	A \or \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2)