Step |
Hyp |
Ref |
Expression |
1 |
|
2dim.j |
|- .\/ = ( join ` K ) |
2 |
|
2dim.c |
|- C = ( |
3 |
|
2dim.a |
|- A = ( Atoms ` K ) |
4 |
1 2 3
|
2dim |
|- ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) |
5 |
|
r19.42v |
|- ( E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) <-> ( P C ( P .\/ q ) /\ E. r e. A ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) |
6 |
5
|
simplbi |
|- ( E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) -> P C ( P .\/ q ) ) |
7 |
6
|
reximi |
|- ( E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) -> E. q e. A P C ( P .\/ q ) ) |
8 |
4 7
|
syl |
|- ( ( K e. HL /\ P e. A ) -> E. q e. A P C ( P .\/ q ) ) |