theorem anrasss (a b c d: wff): $ a /\ b /\ c -> d $ > $ a /\ c /\ b -> d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | a /\ b /\ c -> d |
|
| 2 | anll | a /\ c /\ b -> a |
|
| 3 | anr | a /\ c /\ b -> b |
|
| 4 | 2, 3 | iand | a /\ c /\ b -> a /\ b |
| 5 | anlr | a /\ c /\ b -> c |
|
| 6 | 1, 4, 5 | sylan | a /\ c /\ b -> d |