Theorem anandi 674

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 567	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 625	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 654	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 279	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anandi3  1098  an3andi  1478  2eu4  2739  inrab  4275  uniin  4862  xpco  6140  fin  6559  fndmin  6815  wfrlem5  7959  oaord  8173  nnaord  8245  ixpin  8487  isffth2  17186  fucinv  17243  setcinv  17350  unocv  20824  bldisj  23008  blin  23031  mbfmax  24250  mbfimaopnlem  24256  mbfaddlem  24261  i1faddlem  24294  i1fmullem  24295  lgsquadlem3  25958  numedglnl  26929  wlkeq  27415  ofpreima  30410  cntzun  30695  ordtconnlem1  31167  dfpo2  32991  fneval  33700  mbfposadd  34954  anan  35514  exanres  35567  iss2  35616  1cossres  35689  prtlem70  36008  fz1eqin  39386  fgraphopab  39830  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347  itsclc0b  44779