theorem imor (a b c: wff): $ a \/ b -> c <-> (a -> c) /\ (b -> c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orl | a -> a \/ b |
|
| 2 | 1 | imim1i | (a \/ b -> c) -> a -> c |
| 3 | orr | b -> a \/ b |
|
| 4 | 3 | imim1i | (a \/ b -> c) -> b -> c |
| 5 | 2, 4 | iand | (a \/ b -> c) -> (a -> c) /\ (b -> c) |
| 6 | eor | (a -> c) -> (b -> c) -> a \/ b -> c |
|
| 7 | 6 | imp | (a -> c) /\ (b -> c) -> a \/ b -> c |
| 8 | 5, 7 | ibii | a \/ b -> c <-> (a -> c) /\ (b -> c) |