![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > caov4d | GIF version |
Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
Ref | Expression |
---|---|
caovd.1 | ⊢ (φ → A ∈ 𝑆) |
caovd.2 | ⊢ (φ → B ∈ 𝑆) |
caovd.3 | ⊢ (φ → 𝐶 ∈ 𝑆) |
caovd.com | ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x)) |
caovd.ass | ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))) |
caovd.4 | ⊢ (φ → 𝐷 ∈ 𝑆) |
caovd.cl | ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) |
Ref | Expression |
---|---|
caov4d | ⊢ (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = ((A𝐹𝐶)𝐹(B𝐹𝐷))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caovd.2 | . . . 4 ⊢ (φ → B ∈ 𝑆) | |
2 | caovd.3 | . . . 4 ⊢ (φ → 𝐶 ∈ 𝑆) | |
3 | caovd.4 | . . . 4 ⊢ (φ → 𝐷 ∈ 𝑆) | |
4 | caovd.com | . . . 4 ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x)) | |
5 | caovd.ass | . . . 4 ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))) | |
6 | 1, 2, 3, 4, 5 | caov12d 5624 | . . 3 ⊢ (φ → (B𝐹(𝐶𝐹𝐷)) = (𝐶𝐹(B𝐹𝐷))) |
7 | 6 | oveq2d 5471 | . 2 ⊢ (φ → (A𝐹(B𝐹(𝐶𝐹𝐷))) = (A𝐹(𝐶𝐹(B𝐹𝐷)))) |
8 | caovd.1 | . . 3 ⊢ (φ → A ∈ 𝑆) | |
9 | caovd.cl | . . . 4 ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) | |
10 | 9, 2, 3 | caovcld 5596 | . . 3 ⊢ (φ → (𝐶𝐹𝐷) ∈ 𝑆) |
11 | 5, 8, 1, 10 | caovassd 5602 | . 2 ⊢ (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = (A𝐹(B𝐹(𝐶𝐹𝐷)))) |
12 | 9, 1, 3 | caovcld 5596 | . . 3 ⊢ (φ → (B𝐹𝐷) ∈ 𝑆) |
13 | 5, 8, 2, 12 | caovassd 5602 | . 2 ⊢ (φ → ((A𝐹𝐶)𝐹(B𝐹𝐷)) = (A𝐹(𝐶𝐹(B𝐹𝐷)))) |
14 | 7, 11, 13 | 3eqtr4d 2079 | 1 ⊢ (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = ((A𝐹𝐶)𝐹(B𝐹𝐷))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 884 = wceq 1242 ∈ wcel 1390 (class class class)co 5455 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-3an 886 df-tru 1245 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ral 2305 df-rex 2306 df-v 2553 df-un 2916 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-br 3756 df-iota 4810 df-fv 4853 df-ov 5458 |
This theorem is referenced by: caov411d 5628 caov42d 5629 ecopovtrn 6139 ecopovtrng 6142 addcmpblnq 6351 mulcmpblnq 6352 ordpipqqs 6358 distrnqg 6371 ltsonq 6382 ltanqg 6384 ltmnqg 6385 addcmpblnq0 6426 mulcmpblnq0 6427 distrnq0 6442 prarloclemlo 6477 addlocprlemeqgt 6515 addcanprleml 6588 recexprlem1ssl 6605 recexprlem1ssu 6606 mulcmpblnrlemg 6668 distrsrg 6687 ltasrg 6698 mulgt0sr 6704 axdistr 6758 |
Copyright terms: Public domain | W3C validator |