Metamath Proof Explorer


Theorem adddii

Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994)

Ref Expression
Hypotheses axi.1 A
axi.2 B
axi.3 C
Assertion adddii A B + C = A B + A C

Proof

Step Hyp Ref Expression
1 axi.1 A
2 axi.2 B
3 axi.3 C
4 adddi A B C A B + C = A B + A C
5 1 2 3 4 mp3an A B + C = A B + A C