Theorem orr ≪ | index | src | ≫

theorem orr (a b: wff): $ b -> a \/ b $;

Step	Hyp	Ref	Expression
1		ax_1	b -> ~a -> b
2	1	conv or	b -> a \/ b

Axiom use

axs_prop_calc (ax_1)