theorem anim2a (a b c: wff): $ (a -> b -> c) -> a /\ b -> a /\ c $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anrl | (a -> b -> c) /\ (a /\ b) -> a |
|
| 2 | anrr | (a -> b -> c) /\ (a /\ b) -> b |
|
| 3 | anl | (a -> b -> c) /\ (a /\ b) -> a -> b -> c |
|
| 4 | 1, 3 | mpd | (a -> b -> c) /\ (a /\ b) -> b -> c |
| 5 | 2, 4 | mpd | (a -> b -> c) /\ (a /\ b) -> c |
| 6 | 1, 5 | iand | (a -> b -> c) /\ (a /\ b) -> a /\ c |
| 7 | 6 | exp | (a -> b -> c) -> a /\ b -> a /\ c |