Theorem anandi 677

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 625	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 657	. 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  1485  2eu4  2655  inrab  4256  uniin  4874  xpco  6253  dfpo2  6260  fin  6720  fndmin  6997  oaord  8482  nnaord  8555  ixpin  8871  isffth2  17885  fucinv  17943  setcinv  18057  rngcinv  20614  ringcinv  20648  unocv  21660  bldisj  24363  blin  24386  mbfmax  25616  mbfimaopnlem  25622  mbfaddlem  25627  i1faddlem  25660  i1fmullem  25661  lgsquadlem3  27345  numedglnl  29213  wlkeq  29702  ofpreima  32738  cntzun  33140  isunit2  33301  ordtconnlem1  34068  fneval  36534  mbfposadd  37988  anan  38556  exanres  38622  iss2  38665  1cossres  38840  prtlem70  39303  fz1eqin  43201  fgraphopab  43631  rngcinvALTV  48752  ringcinvALTV  48786  itsclc0b  49248  i0oii  49395  io1ii  49396  catcinv  49874