Theorem orim | index | src |

theorem orim (a b c d: wff): $ (a -> b) -> (c -> d) -> a \/ c -> b \/ d $;
StepHypRefExpression
1 orim1
(a -> b) -> a \/ c -> b \/ c
2 1 anwl
(a -> b) /\ (c -> d) -> a \/ c -> b \/ c
3 orim2
(c -> d) -> b \/ c -> b \/ d
4 3 anwr
(a -> b) /\ (c -> d) -> b \/ c -> b \/ d
5 2, 4 syld
(a -> b) /\ (c -> d) -> a \/ c -> b \/ d
6 5 exp
(a -> b) -> (c -> d) -> a \/ c -> b \/ d

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)