theorem eor (a b c: wff): $ (a -> c) -> (b -> c) -> a \/ b -> c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anl | (a -> c) /\ (b -> c) -> a -> c |
|
2 | anr | (a -> c) /\ (b -> c) -> b -> c |
|
3 | 1, 2 | eord | (a -> c) /\ (b -> c) -> a \/ b -> c |
4 | 3 | exp | (a -> c) -> (b -> c) -> a \/ b -> c |