![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anandi | Structured version Visualization version Unicode version |
Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.) |
Ref | Expression |
---|---|
anandi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anidm 649 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi1i 700 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | an4 832 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitr3i 255 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 df-an 373 |
This theorem is referenced by: anandi3 998 an3andi 1381 2eu4 2384 inrab 3714 uniin 4217 xpco 5375 fin 5761 fndmin 5987 oaord 7245 nnaord 7317 ixpin 7544 isffth2 15814 fucinv 15871 setcinv 15978 unocv 19236 bldisj 21406 blin 21429 mbfmax 22598 mbfimaopnlem 22604 mbfaddlem 22609 i1faddlem 22644 i1fmullem 22645 lgsquadlem3 24277 2wlkeq 25428 ofpreima 28261 ordtconlem1 28723 dfpo2 30388 fneval 31001 mbfposadd 31981 prtlem70 32419 fz1eqin 35605 fgraphopab 36081 rngcinv 39970 rngcinvALTV 39982 ringcinv 40021 ringcinvALTV 40045 |
Copyright terms: Public domain | W3C validator |