Theorem em ≪ | index | src | ≫

theorem em (p: wff): $ p \/ ~p $;

Step	Hyp	Ref	Expression
1		id	~p -> ~p
2	1	conv or	p \/ ~p

Axiom use

axs_prop_calc (ax_1, ax_2, ax_mp)