Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
|- ( B = C -> ( B e. A <-> C e. A ) ) |
2 |
1
|
biimpcd |
|- ( B e. A -> ( B = C -> C e. A ) ) |
3 |
2
|
adantl |
|- ( ( A e. P. /\ B e. A ) -> ( B = C -> C e. A ) ) |
4 |
|
prcdnq |
|- ( ( A e. P. /\ B e. A ) -> ( C C e. A ) ) |
5 |
3 4
|
jaod |
|- ( ( A e. P. /\ B e. A ) -> ( ( B = C \/ C C e. A ) ) |
6 |
5
|
con3d |
|- ( ( A e. P. /\ B e. A ) -> ( -. C e. A -> -. ( B = C \/ C |
7 |
6
|
adantr |
|- ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( -. C e. A -> -. ( B = C \/ C |
8 |
|
elprnq |
|- ( ( A e. P. /\ B e. A ) -> B e. Q. ) |
9 |
|
ltsonq |
|- |
10 |
|
sotric |
|- ( ( ( B -. ( B = C \/ C |
11 |
9 10
|
mpan |
|- ( ( B e. Q. /\ C e. Q. ) -> ( B -. ( B = C \/ C |
12 |
8 11
|
sylan |
|- ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( B -. ( B = C \/ C |
13 |
7 12
|
sylibrd |
|- ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( -. C e. A -> B |