Step |
Hyp |
Ref |
Expression |
1 |
|
sonr |
|- ( ( R Or A /\ B e. A ) -> -. B R B ) |
2 |
1
|
adantrr |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> -. B R B ) |
3 |
|
pm1.2 |
|- ( ( B R B \/ B R B ) -> B R B ) |
4 |
2 3
|
nsyl |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> -. ( B R B \/ B R B ) ) |
5 |
|
breq2 |
|- ( B = C -> ( B R B <-> B R C ) ) |
6 |
|
breq1 |
|- ( B = C -> ( B R B <-> C R B ) ) |
7 |
5 6
|
orbi12d |
|- ( B = C -> ( ( B R B \/ B R B ) <-> ( B R C \/ C R B ) ) ) |
8 |
7
|
notbid |
|- ( B = C -> ( -. ( B R B \/ B R B ) <-> -. ( B R C \/ C R B ) ) ) |
9 |
4 8
|
syl5ibcom |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C -> -. ( B R C \/ C R B ) ) ) |
10 |
9
|
con2d |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B R C \/ C R B ) -> -. B = 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 |
|
or12 |
|- ( ( B R C \/ ( B = C \/ C R B ) ) <-> ( B = C \/ ( B R C \/ C R B ) ) ) |
15 |
13 14
|
sylib |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C \/ ( B R C \/ C R B ) ) ) |
16 |
15
|
ord |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( -. B = C -> ( B R C \/ C R B ) ) ) |
17 |
10 16
|
impbid |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B R C \/ C R B ) <-> -. B = C ) ) |
18 |
17
|
con2bid |
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> -. ( B R C \/ C R B ) ) ) |