Theorem anrotri | index | src |

theorem anrotri (a b c d: wff): $ b /\ d -> a $ > $ b /\ c /\ d -> a /\ c $;
StepHypRefExpression
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

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)