Theorem anandi 688

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 574	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 635	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 668	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 280	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anandi3  1119  an3andi  1513  2eu4  2682  inrab  4270  uniinOLD  4898  xpco  6292  dfpo2  6299  fin  6760  fndmin  7042  oaord  8533  nnaord  8606  ixpin  8922  isffth2  17976  fucinv  18034  setcinv  18148  rngcinv  20723  ringcinv  20757  unocv  21811  bldisj  24536  blin  24559  mbfmax  25789  mbfimaopnlem  25795  mbfaddlem  25800  i1faddlem  25833  i1fmullem  25834  lgsquadlem3  27524  numedglnl  29472  wlkeq  29961  ofpreima  32988  cntzun  33377  isunit2  33537  ordtconnlem1  34292  fneval  36841  mbfposadd  38296  anan  38862  exanres  38928  iss2  38971  1cossres  39146  prtlem70  39609  fz1eqin  43480  fgraphopab  43910  rngcinvALTV  49018  ringcinvALTV  49052  itsclc0b  49529  i0oii  49675  io1ii  49676  catcinv  50154