Step |
Hyp |
Ref |
Expression |
1 |
|
sonr |
|- ( ( R Or A /\ B e. A ) -> -. B R B ) |
2 |
|
breq2 |
|- ( B = C -> ( B R B <-> B R C ) ) |
3 |
2
|
notbid |
|- ( B = C -> ( -. B R B <-> -. B R C ) ) |
4 |
1 3
|
syl5ibcom |
|- ( ( R Or A /\ B e. A ) -> ( B = C -> -. B R C ) ) |
5 |
4
|
adantrr |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C -> -. B R C ) ) |
6 |
|
so2nr |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) ) |
7 |
|
imnan |
|- ( ( B R C -> -. C R B ) <-> -. ( B R C /\ C R B ) ) |
8 |
6 7
|
sylibr |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C -> -. C R B ) ) |
9 |
8
|
con2d |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( C R B -> -. B R C ) ) |
10 |
5 9
|
jaod |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B = C \/ C R B ) -> -. B R C ) ) |
11 |
|
solin |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ B = C \/ C R B ) ) |
12 |
|
3orass |
|- ( ( B R C \/ B = C \/ C R B ) <-> ( B R C \/ ( B = C \/ C R B ) ) ) |
13 |
11 12
|
sylib |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ ( B = C \/ C R B ) ) ) |
14 |
13
|
ord |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( -. B R C -> ( B = C \/ C R B ) ) ) |
15 |
10 14
|
impbid |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B = C \/ C R B ) <-> -. B R C ) ) |
16 |
15
|
con2bid |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C <-> -. ( B = C \/ C R B ) ) ) |