Theorem em | index | src |

theorem em (p: wff): $ p \/ ~p $;
StepHypRefExpression
1 id
~p -> ~p
2 1 conv or
p \/ ~p

Axiom use

axs_prop_calc (ax_1, ax_2, ax_mp)