| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3dim0.j |
|- .\/ = ( join ` K ) |
| 2 |
|
3dim0.l |
|- .<_ = ( le ` K ) |
| 3 |
|
3dim0.a |
|- A = ( Atoms ` K ) |
| 4 |
|
neeq1 |
|- ( P = Q -> ( P =/= R <-> Q =/= R ) ) |
| 5 |
|
oveq1 |
|- ( P = Q -> ( P .\/ R ) = ( Q .\/ R ) ) |
| 6 |
5
|
breq2d |
|- ( P = Q -> ( S .<_ ( P .\/ R ) <-> S .<_ ( Q .\/ R ) ) ) |
| 7 |
6
|
notbid |
|- ( P = Q -> ( -. S .<_ ( P .\/ R ) <-> -. S .<_ ( Q .\/ R ) ) ) |
| 8 |
5
|
oveq1d |
|- ( P = Q -> ( ( P .\/ R ) .\/ S ) = ( ( Q .\/ R ) .\/ S ) ) |
| 9 |
8
|
breq2d |
|- ( P = Q -> ( T .<_ ( ( P .\/ R ) .\/ S ) <-> T .<_ ( ( Q .\/ R ) .\/ S ) ) ) |
| 10 |
9
|
notbid |
|- ( P = Q -> ( -. T .<_ ( ( P .\/ R ) .\/ S ) <-> -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) |
| 11 |
4 7 10
|
3anbi123d |
|- ( P = Q -> ( ( P =/= R /\ -. S .<_ ( P .\/ R ) /\ -. T .<_ ( ( P .\/ R ) .\/ S ) ) <-> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) ) |
| 12 |
11
|
biimparc |
|- ( ( ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) /\ P = Q ) -> ( P =/= R /\ -. S .<_ ( P .\/ R ) /\ -. T .<_ ( ( P .\/ R ) .\/ S ) ) ) |