Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme31sde.c |
⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) |
2 |
|
cdleme31sde.e |
⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) |
3 |
|
cdleme31sde.x |
⊢ 𝑌 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) ) |
4 |
|
cdleme31sde.z |
⊢ 𝑍 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) |
5 |
2
|
csbeq2i |
⊢ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = ⦋ 𝑆 / 𝑡 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) |
6 |
|
nfcvd |
⊢ ( 𝑆 ∈ 𝐴 → Ⅎ 𝑡 ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) ) |
7 |
|
oveq1 |
⊢ ( 𝑡 = 𝑆 → ( 𝑡 ∨ 𝑈 ) = ( 𝑆 ∨ 𝑈 ) ) |
8 |
|
oveq2 |
⊢ ( 𝑡 = 𝑆 → ( 𝑃 ∨ 𝑡 ) = ( 𝑃 ∨ 𝑆 ) ) |
9 |
8
|
oveq1d |
⊢ ( 𝑡 = 𝑆 → ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) |
10 |
9
|
oveq2d |
⊢ ( 𝑡 = 𝑆 → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) ) |
11 |
7 10
|
oveq12d |
⊢ ( 𝑡 = 𝑆 → ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) ) ) |
12 |
11 1 3
|
3eqtr4g |
⊢ ( 𝑡 = 𝑆 → 𝐷 = 𝑌 ) |
13 |
|
oveq2 |
⊢ ( 𝑡 = 𝑆 → ( 𝑠 ∨ 𝑡 ) = ( 𝑠 ∨ 𝑆 ) ) |
14 |
13
|
oveq1d |
⊢ ( 𝑡 = 𝑆 → ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) = ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) |
15 |
12 14
|
oveq12d |
⊢ ( 𝑡 = 𝑆 → ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) = ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) |
16 |
15
|
oveq2d |
⊢ ( 𝑡 = 𝑆 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) ) |
17 |
6 16
|
csbiegf |
⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑡 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) ) |
18 |
5 17
|
eqtrid |
⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) ) |
19 |
18
|
csbeq2dv |
⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) ) |
20 |
|
eqid |
⊢ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) |
21 |
20 4
|
cdleme31se |
⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = 𝑍 ) |
22 |
19 21
|
sylan9eqr |
⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ⦋ 𝑅 / 𝑠 ⦌ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = 𝑍 ) |