![]() |
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 | ⊢ (𝜑 → 𝐴 ∈ 𝑆) |
caovd.2 | ⊢ (𝜑 → 𝐵 ∈ 𝑆) |
caovd.3 | ⊢ (𝜑 → 𝐶 ∈ 𝑆) |
caovd.com | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) |
caovd.ass | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) |
caovd.4 | ⊢ (𝜑 → 𝐷 ∈ 𝑆) |
caovd.cl | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
Ref | Expression |
---|---|
caov4d | ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caovd.2 | . . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑆) | |
2 | caovd.3 | . . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑆) | |
3 | caovd.4 | . . . 4 ⊢ (𝜑 → 𝐷 ∈ 𝑆) | |
4 | caovd.com | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) | |
5 | caovd.ass | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) | |
6 | 1, 2, 3, 4, 5 | caov12d 5760 | . . 3 ⊢ (𝜑 → (𝐵𝐹(𝐶𝐹𝐷)) = (𝐶𝐹(𝐵𝐹𝐷))) |
7 | 6 | oveq2d 5606 | . 2 ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹(𝐶𝐹𝐷))) = (𝐴𝐹(𝐶𝐹(𝐵𝐹𝐷)))) |
8 | caovd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑆) | |
9 | caovd.cl | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) | |
10 | 9, 2, 3 | caovcld 5732 | . . 3 ⊢ (𝜑 → (𝐶𝐹𝐷) ∈ 𝑆) |
11 | 5, 8, 1, 10 | caovassd 5738 | . 2 ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = (𝐴𝐹(𝐵𝐹(𝐶𝐹𝐷)))) |
12 | 9, 1, 3 | caovcld 5732 | . . 3 ⊢ (𝜑 → (𝐵𝐹𝐷) ∈ 𝑆) |
13 | 5, 8, 2, 12 | caovassd 5738 | . 2 ⊢ (𝜑 → ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)) = (𝐴𝐹(𝐶𝐹(𝐵𝐹𝐷)))) |
14 | 7, 11, 13 | 3eqtr4d 2125 | 1 ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 = wceq 1285 ∈ wcel 1434 (class class class)co 5590 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-v 2614 df-un 2988 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-br 3812 df-iota 4933 df-fv 4976 df-ov 5593 |
This theorem is referenced by: caov411d 5764 caov42d 5765 ecopovtrn 6318 ecopovtrng 6321 addcmpblnq 6828 mulcmpblnq 6829 ordpipqqs 6835 distrnqg 6848 ltsonq 6859 ltanqg 6861 ltmnqg 6862 addcmpblnq0 6904 mulcmpblnq0 6905 distrnq0 6920 prarloclemlo 6955 addlocprlemeqgt 6993 addcanprleml 7075 recexprlem1ssl 7094 recexprlem1ssu 7095 mulcmpblnrlemg 7188 distrsrg 7207 ltasrg 7218 mulgt0sr 7225 prsradd 7233 axdistr 7311 |
Copyright terms: Public domain | W3C validator |