ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-distr Unicode version

Axiom ax-distr 7045
Description: Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7005. Proofs should normally use adddi 7070 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
ax-distr  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )

Detailed syntax breakdown of Axiom ax-distr
StepHypRef Expression
1 cA . . . 4  class  A
2 cc 6944 . . . 4  class  CC
31, 2wcel 1409 . . 3  wff  A  e.  CC
4 cB . . . 4  class  B
54, 2wcel 1409 . . 3  wff  B  e.  CC
6 cC . . . 4  class  C
76, 2wcel 1409 . . 3  wff  C  e.  CC
83, 5, 7w3a 896 . 2  wff  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )
9 caddc 6949 . . . . 5  class  +
104, 6, 9co 5539 . . . 4  class  ( B  +  C )
11 cmul 6951 . . . 4  class  x.
121, 10, 11co 5539 . . 3  class  ( A  x.  ( B  +  C ) )
131, 4, 11co 5539 . . . 4  class  ( A  x.  B )
141, 6, 11co 5539 . . . 4  class  ( A  x.  C )
1513, 14, 9co 5539 . . 3  class  ( ( A  x.  B )  +  ( A  x.  C ) )
1612, 15wceq 1259 . 2  wff  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
178, 16wi 4 1  wff  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
This axiom is referenced by:  adddi  7070
  Copyright terms: Public domain W3C validator