# Metamath Proof Explorer

## Axiom ax-distr

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr . Proofs should normally use adddi instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion ax-distr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}\left({B}+{C}\right)={A}{B}+{A}{C}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cc ${class}ℂ$
2 0 1 wcel ${wff}{A}\in ℂ$
3 cB ${class}{B}$
4 3 1 wcel ${wff}{B}\in ℂ$
5 cC ${class}{C}$
6 5 1 wcel ${wff}{C}\in ℂ$
7 2 4 6 w3a ${wff}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)$
8 cmul ${class}×$
9 caddc ${class}+$
10 3 5 9 co ${class}\left({B}+{C}\right)$
11 0 10 8 co ${class}{A}\left({B}+{C}\right)$
12 0 3 8 co ${class}{A}{B}$
13 0 5 8 co ${class}{A}{C}$
14 12 13 9 co ${class}\left({A}{B}+{A}{C}\right)$
15 11 14 wceq ${wff}{A}\left({B}+{C}\right)={A}{B}+{A}{C}$
16 7 15 wi ${wff}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}\left({B}+{C}\right)={A}{B}+{A}{C}\right)$