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  1101  an3andi  1484  2eu4  2654  inrab  4291  uniin  4907  xpco  6278  dfpo2  6285  fin  6757  fndmin  7034  wfrlem5OLD  8325  oaord  8557  nnaord  8629  ixpin  8935  isffth2  17929  fucinv  17987  setcinv  18101  rngcinv  20595  ringcinv  20629  unocv  21638  bldisj  24335  blin  24358  mbfmax  25600  mbfimaopnlem  25606  mbfaddlem  25611  i1faddlem  25644  i1fmullem  25645  lgsquadlem3  27343  numedglnl  29069  wlkeq  29560  ofpreima  32589  cntzun  33008  isunit2  33181  ordtconnlem1  33901  fneval  36316  mbfposadd  37637  anan  38193  exanres  38259  iss2  38308  1cossres  38393  prtlem70  38821  fz1eqin  42739  fgraphopab  43174  rngcinvALTV  48199  ringcinvALTV  48233  itsclc0b  48700  i0oii  48842  io1ii  48843