theorem orim (a b c d: wff): $ (a -> b) -> (c -> d) -> a \/ c -> b \/ d $;
Step | Hyp | Ref | Expression |
---|---|---|---|
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 |