Theorem anandi 682

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 569	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 630	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 662	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 278	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anandi3  1107  an3andi  1490  2eu4  2659  inrab  4251  uniin  4869  xpco  6247  dfpo2  6254  fin  6714  fndmin  6993  oaord  8479  nnaord  8552  ixpin  8868  isffth2  17883  fucinv  17941  setcinv  18055  rngcinv  20616  ringcinv  20650  unocv  21662  bldisj  24388  blin  24411  mbfmax  25641  mbfimaopnlem  25647  mbfaddlem  25652  i1faddlem  25685  i1fmullem  25686  lgsquadlem3  27370  numedglnl  29238  wlkeq  29727  ofpreima  32764  cntzun  33167  isunit2  33328  ordtconnlem1  34115  fneval  36587  mbfposadd  38041  anan  38609  exanres  38675  iss2  38718  1cossres  38893  prtlem70  39356  fz1eqin  43225  fgraphopab  43655  rngcinvALTV  48774  ringcinvALTV  48808  itsclc0b  49270  i0oii  49417  io1ii  49418  catcinv  49896