Theorem orimd ≪ | index | src | ≫ 

theorem orimd (a b c d e: wff):
  $ a -> b -> c $ >
  $ a -> d -> e $ >
  $ a -> b \/ d -> c \/ e $;
StepHypRefExpression
1 orl 
c -> c \/ e
2 hyp h1 
a -> b -> c
3 1, 2 syl6 
a -> b -> c \/ e
4 orr 
e -> c \/ e
5 hyp h2 
a -> d -> e
6 4, 5 syl6 
a -> d -> c \/ e
7 3, 6 eord 
a -> b \/ d -> c \/ e

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)