Theorem anandi 689

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anandi3  1119  an3andi  1513  2eu4  2680  inrab  4262  uniinOLD  4892  xpco  6285  dfpo2  6292  fin  6754  fndmin  7036  oaord  8539  nnaord  8612  ixpin  8935  isffth2  18073  fucinv  18131  setcinv  18245  rngcinv  20869  ringcinv  20903  unocv  21966  bldisj  24697  blin  24720  mbfmax  25950  mbfimaopnlem  25956  mbfaddlem  25961  i1faddlem  25994  i1fmullem  25995  lgsquadlem3  27691  numedglnl  29704  wlkeq  30196  ofpreima  33241  cntzun  33622  isunit2  33782  ordtconnlem1  34538  fneval  37110  mbfposadd  38553  anan  39135  exanres  39201  iss2  39244  1cossres  39419  prtlem70  39882  fz1eqin  43733  fgraphopab  44163  rngcinvALTV  49317  ringcinvALTV  49351  itsclc0b  49828  i0oii  49972  io1ii  49973  catcinv  50451