Theorem anandi 672

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 623	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 652	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 276	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anandi3  1100  an3andi  1480  2eu4  2656  inrab  4237  uniin  4862  xpco  6181  dfpo2  6188  fin  6638  fndmin  6904  wfrlem5OLD  8115  oaord  8340  nnaord  8412  ixpin  8669  isffth2  17548  fucinv  17607  setcinv  17721  unocv  20797  bldisj  23459  blin  23482  mbfmax  24718  mbfimaopnlem  24724  mbfaddlem  24729  i1faddlem  24762  i1fmullem  24763  lgsquadlem3  26435  numedglnl  27417  wlkeq  27903  ofpreima  30904  cntzun  31222  ordtconnlem1  31776  fneval  34468  mbfposadd  35751  anan  36306  exanres  36357  iss2  36406  1cossres  36479  prtlem70  36798  fz1eqin  40507  fgraphopab  40951  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  itsclc0b  46006  i0oii  46101  io1ii  46102