Theorem anandi 676

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 564	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 624	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 656	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 277	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anandi3  1102  an3andi  1484  2eu4  2655  inrab  4316  uniin  4931  xpco  6309  dfpo2  6316  fin  6788  fndmin  7065  wfrlem5OLD  8353  oaord  8585  nnaord  8657  ixpin  8963  isffth2  17963  fucinv  18021  setcinv  18135  rngcinv  20637  ringcinv  20671  unocv  21698  bldisj  24408  blin  24431  mbfmax  25684  mbfimaopnlem  25690  mbfaddlem  25695  i1faddlem  25728  i1fmullem  25729  lgsquadlem3  27426  numedglnl  29161  wlkeq  29652  ofpreima  32675  cntzun  33071  isunit2  33244  ordtconnlem1  33923  fneval  36353  mbfposadd  37674  anan  38230  exanres  38296  iss2  38345  1cossres  38430  prtlem70  38858  fz1eqin  42780  fgraphopab  43215  rngcinvALTV  48192  ringcinvALTV  48226  itsclc0b  48693  i0oii  48817  io1ii  48818