theorem animd (a b c d e: wff): $ a -> b -> c $ > $ a -> d -> e $ > $ a -> b /\ d -> c /\ e $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anl | b /\ d -> b |
|
| 2 | hyp h1 | a -> b -> c |
|
| 3 | 1, 2 | syl5 | a -> b /\ d -> c |
| 4 | 3 | imp | a /\ (b /\ d) -> c |
| 5 | anr | b /\ d -> d |
|
| 6 | hyp h2 | a -> d -> e |
|
| 7 | 5, 6 | syl5 | a -> b /\ d -> e |
| 8 | 7 | imp | a /\ (b /\ d) -> e |
| 9 | 4, 8 | iand | a /\ (b /\ d) -> c /\ e |
| 10 | 9 | exp | a -> b /\ d -> c /\ e |