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  2649  inrab  4282  uniin  4898  xpco  6265  dfpo2  6272  fin  6743  fndmin  7020  oaord  8514  nnaord  8586  ixpin  8899  isffth2  17887  fucinv  17945  setcinv  18059  rngcinv  20553  ringcinv  20587  unocv  21596  bldisj  24293  blin  24316  mbfmax  25557  mbfimaopnlem  25563  mbfaddlem  25568  i1faddlem  25601  i1fmullem  25602  lgsquadlem3  27300  numedglnl  29078  wlkeq  29569  ofpreima  32596  cntzun  33015  isunit2  33198  ordtconnlem1  33921  fneval  36347  mbfposadd  37668  anan  38224  exanres  38290  iss2  38333  1cossres  38427  prtlem70  38857  fz1eqin  42764  fgraphopab  43199  rngcinvALTV  48268  ringcinvALTV  48302  itsclc0b  48765  i0oii  48912  io1ii  48913  catcinv  49392