theorem imandi (a b c: wff): $ a -> b /\ c <-> (a -> b) /\ (a -> c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anl | b /\ c -> b |
|
| 2 | 1 | imim2i | (a -> b /\ c) -> a -> b |
| 3 | anr | b /\ c -> c |
|
| 4 | 3 | imim2i | (a -> b /\ c) -> a -> c |
| 5 | 2, 4 | iand | (a -> b /\ c) -> (a -> b) /\ (a -> c) |
| 6 | mpcom | a -> (a -> b) -> b |
|
| 7 | mpcom | a -> (a -> c) -> c |
|
| 8 | 6, 7 | animd | a -> (a -> b) /\ (a -> c) -> b /\ c |
| 9 | 8 | com12 | (a -> b) /\ (a -> c) -> a -> b /\ c |
| 10 | 5, 9 | ibii | a -> b /\ c <-> (a -> b) /\ (a -> c) |