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