theorem anroti (a b c d: wff): $ a -> b /\ d $ > $ a /\ c -> b /\ c /\ d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anrass | b /\ d /\ c <-> b /\ c /\ d |
|
| 2 | anim1 | (a -> b /\ d) -> a /\ c -> b /\ d /\ c |
|
| 3 | hyp h | a -> b /\ d |
|
| 4 | 2, 3 | ax_mp | a /\ c -> b /\ d /\ c |
| 5 | 1, 4 | sylib | a /\ c -> b /\ c /\ d |