Theorem eord ≪ | index | src | ≫

theorem eord (a b c d: wff):
  $ a -> b -> d $ >
  $ a -> c -> d $ >
  $ a -> b \/ c -> d $;

Step	Hyp	Ref	Expression
1		hyp h1	a -> b -> d
2	1	com12	b -> a -> d
3		hyp h2	a -> c -> d
4	3	com12	c -> a -> d
5	2, 4	eori	b \/ c -> a -> d
6	5	com12	a -> b \/ c -> d

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)