theorem anim (a b c d: wff): $ (a -> b) -> (c -> d) -> a /\ c -> b /\ d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anl | (a -> b) /\ (c -> d) -> a -> b |
|
| 2 | 1 | anim1d | (a -> b) /\ (c -> d) -> a /\ c -> b /\ c |
| 3 | anr | (a -> b) /\ (c -> d) -> c -> d |
|
| 4 | 3 | anim2d | (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 |