Step |
Hyp |
Ref |
Expression |
1 |
|
3dim0.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
2 |
|
3dim0.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
3dim0.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
neeq1 |
⊢ ( 𝑃 = 𝑄 → ( 𝑃 ≠ 𝑅 ↔ 𝑄 ≠ 𝑅 ) ) |
5 |
|
oveq1 |
⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) |
6 |
5
|
breq2d |
⊢ ( 𝑃 = 𝑄 → ( 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) |
7 |
6
|
notbid |
⊢ ( 𝑃 = 𝑄 → ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ↔ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) |
8 |
5
|
oveq1d |
⊢ ( 𝑃 = 𝑄 → ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) |
9 |
8
|
breq2d |
⊢ ( 𝑃 = 𝑄 → ( 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ↔ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) |
10 |
9
|
notbid |
⊢ ( 𝑃 = 𝑄 → ( ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ↔ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) |
11 |
4 7 10
|
3anbi123d |
⊢ ( 𝑃 = 𝑄 → ( ( 𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) ↔ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ) |
12 |
11
|
biimparc |
⊢ ( ( ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) ) |