MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul4 Structured version   Visualization version   GIF version

Theorem mul4 11384
Description: Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
Assertion
Ref Expression
mul4 (((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง (๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท)))

Proof of Theorem mul4
StepHypRef Expression
1 mul32 11382 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) ยท ๐ต))
21oveq1d 7426 . . . 4 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท))
323expa 1118 . . 3 (((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง ๐ถ โˆˆ โ„‚) โ†’ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท))
43adantrr 715 . 2 (((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง (๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท))
5 mulcl 11196 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด ยท ๐ต) โˆˆ โ„‚)
6 mulass 11200 . . . 4 (((๐ด ยท ๐ต) โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚) โ†’ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)))
763expb 1120 . . 3 (((๐ด ยท ๐ต) โˆˆ โ„‚ โˆง (๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)))
85, 7sylan 580 . 2 (((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง (๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)))
9 mulcl 11196 . . . 4 ((๐ด โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„‚)
10 mulass 11200 . . . . 5 (((๐ด ยท ๐ถ) โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚) โ†’ (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท)))
11103expb 1120 . . . 4 (((๐ด ยท ๐ถ) โˆˆ โ„‚ โˆง (๐ต โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท)))
129, 11sylan 580 . . 3 (((๐ด โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โˆง (๐ต โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท)))
1312an4s 658 . 2 (((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง (๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท)))
144, 8, 133eqtr3d 2780 1 (((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง (๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚)) โ†’ ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106  (class class class)co 7411  โ„‚cc 11110   ยท cmul 11117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-mulcl 11174  ax-mulcom 11176  ax-mulass 11178
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414
This theorem is referenced by:  mul4r  11385  mul4i  11413  mul4d  11428  recextlem1  11846  divmuldiv  11916  mulexp  14069  demoivreALT  16146  bposlem9  26802
  Copyright terms: Public domain W3C validator