Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adddid | Unicode version |
Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | |
addcld.2 | |
addassd.3 |
Ref | Expression |
---|---|
adddid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 | |
2 | addcld.2 | . 2 | |
3 | addassd.3 | . 2 | |
4 | adddi 7720 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1201 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 wcel 1465 (class class class)co 5742 cc 7586 caddc 7591 cmul 7593 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-distr 7692 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: subdi 8115 mulreim 8334 apadd1 8338 conjmulap 8457 cju 8687 flhalf 10043 modqcyc 10100 addmodlteq 10139 binom2 10371 binom3 10377 sqoddm1div8 10412 bcpasc 10480 remim 10600 mulreap 10604 readd 10609 remullem 10611 imadd 10617 cjadd 10624 bdtrilem 10978 fsummulc2 11185 binomlem 11220 tanval3ap 11348 sinadd 11370 tanaddap 11373 bezoutlemnewy 11611 dvdsmulgcd 11640 lcmgcdlem 11685 tangtx 12846 |
Copyright terms: Public domain | W3C validator |