Theorem orcomb ≪ | index | src | ≫ 

theorem orcomb (a b: wff): $ a \/ b <-> b \/ a $;
StepHypRefExpression
1 orcom 
a \/ b -> b \/ a
2 orcom 
b \/ a -> a \/ b
3 1, 2 ibii 
a \/ b <-> b \/ a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)