Theorem orcom ≪ | index | src | ≫ 

theorem orcom (a b: wff): $ a \/ b -> b \/ a $;
StepHypRefExpression
1 con1 
(~a -> b) -> ~b -> a
2 1 conv or 
a \/ b -> b \/ a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)