Step |
Hyp |
Ref |
Expression |
1 |
|
po2nr |
|- ( ( R Po A /\ ( B e. A /\ D e. A ) ) -> -. ( B R D /\ D R B ) ) |
2 |
1
|
3adantr2 |
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R D /\ D R B ) ) |
3 |
|
df-3an |
|- ( ( B R C /\ C R D /\ D R B ) <-> ( ( B R C /\ C R D ) /\ D R B ) ) |
4 |
|
potr |
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) ) |
5 |
4
|
anim1d |
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( ( B R C /\ C R D ) /\ D R B ) -> ( B R D /\ D R B ) ) ) |
6 |
3 5
|
syl5bi |
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D /\ D R B ) -> ( B R D /\ D R B ) ) ) |
7 |
2 6
|
mtod |
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) ) |