ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  caov4d GIF version

Theorem caov4d 5648
Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
Hypotheses
Ref Expression
caovd.1 (𝜑𝐴𝑆)
caovd.2 (𝜑𝐵𝑆)
caovd.3 (𝜑𝐶𝑆)
caovd.com ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
caovd.ass ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))
caovd.4 (𝜑𝐷𝑆)
caovd.cl ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)
Assertion
Ref Expression
caov4d (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝐷,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧

Proof of Theorem caov4d
StepHypRef Expression
1 caovd.2 . . . 4 (𝜑𝐵𝑆)
2 caovd.3 . . . 4 (𝜑𝐶𝑆)
3 caovd.4 . . . 4 (𝜑𝐷𝑆)
4 caovd.com . . . 4 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
5 caovd.ass . . . 4 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))
61, 2, 3, 4, 5caov12d 5645 . . 3 (𝜑 → (𝐵𝐹(𝐶𝐹𝐷)) = (𝐶𝐹(𝐵𝐹𝐷)))
76oveq2d 5491 . 2 (𝜑 → (𝐴𝐹(𝐵𝐹(𝐶𝐹𝐷))) = (𝐴𝐹(𝐶𝐹(𝐵𝐹𝐷))))
8 caovd.1 . . 3 (𝜑𝐴𝑆)
9 caovd.cl . . . 4 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)
109, 2, 3caovcld 5617 . . 3 (𝜑 → (𝐶𝐹𝐷) ∈ 𝑆)
115, 8, 1, 10caovassd 5623 . 2 (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = (𝐴𝐹(𝐵𝐹(𝐶𝐹𝐷))))
129, 1, 3caovcld 5617 . . 3 (𝜑 → (𝐵𝐹𝐷) ∈ 𝑆)
135, 8, 2, 12caovassd 5623 . 2 (𝜑 → ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)) = (𝐴𝐹(𝐶𝐹(𝐵𝐹𝐷))))
147, 11, 133eqtr4d 2082 1 (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885   = wceq 1243  wcel 1393  (class class class)co 5475
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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-rex 2309  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-iota 4830  df-fv 4873  df-ov 5478
This theorem is referenced by:  caov411d  5649  caov42d  5650  ecopovtrn  6166  ecopovtrng  6169  addcmpblnq  6422  mulcmpblnq  6423  ordpipqqs  6429  distrnqg  6442  ltsonq  6453  ltanqg  6455  ltmnqg  6456  addcmpblnq0  6498  mulcmpblnq0  6499  distrnq0  6514  prarloclemlo  6549  addlocprlemeqgt  6587  addcanprleml  6669  recexprlem1ssl  6688  recexprlem1ssu  6689  mulcmpblnrlemg  6782  distrsrg  6801  ltasrg  6812  mulgt0sr  6819  prsradd  6827  axdistr  6905
  Copyright terms: Public domain W3C validator