Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  anandi Unicode version

Theorem anandi 828
 Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
Assertion
Ref Expression
anandi

Proof of Theorem anandi
StepHypRef Expression
1 anidm 644 . . 3
21anbi1i 695 . 2
3 an4 824 . 2
42, 3bitr3i 251 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  /\wa 369 This theorem is referenced by:  anandi3  987  an3andi  1341  2eu4  2380  inrab  3769  uniin  4269  xpco  5552  fin  5770  fndmin  5994  oaord  7215  nnaord  7287  ixpin  7514  isffth2  15285  fucinv  15342  setcinv  15417  unocv  18711  bldisj  20901  blin  20924  mbfmax  22056  mbfimaopnlem  22062  mbfaddlem  22067  i1faddlem  22100  i1fmullem  22101  lgsquadlem3  23631  2wlkeq  24707  ofpreima  27507  ordtconlem1  27906  dfpo2  29184  mbfposadd  30062  fneval  30170  prtlem70  30592  fz1eqin  30702  fgraphopab  31170  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864 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 185  df-an 371
 Copyright terms: Public domain W3C validator