Theorem
emr
≪
|
index
|
src
|
≫
theorem emr (p: wff): $ ~p \/ p $;
Step
Hyp
Ref
Expression
1
orcom
p \/ ~p -> ~p \/ p
2
em
p \/ ~p
3
1
,
2
ax_mp
~p \/ p
Axiom use
axs_prop_calc
(
ax_1
,
ax_2
,
ax_3
,
ax_mp
)