Theorem anandi 828

Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)

Assertion

Ref	Expression
anandi

Proof of Theorem anandi

Step	Hyp	Ref	Expression
1		anidm 644	. . 3
2	1	anbi1i 695	. 2
3		an4 824	. 2
4	2, 3	bitr3i 251	1

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