Theorem anandi 675

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 655	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 277	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  1479  2eu4  2646  inrab  4307  uniin  4934  xpco  6293  dfpo2  6300  fin  6777  fndmin  7054  wfrlem5OLD  8333  oaord  8567  nnaord  8639  ixpin  8941  isffth2  17904  fucinv  17964  setcinv  18078  rngcinv  20569  ringcinv  20603  unocv  21611  bldisj  24303  blin  24326  mbfmax  25577  mbfimaopnlem  25583  mbfaddlem  25588  i1faddlem  25621  i1fmullem  25622  lgsquadlem3  27314  numedglnl  28956  wlkeq  29447  ofpreima  32450  cntzun  32774  ordtconnlem1  33525  fneval  35836  mbfposadd  37140  anan  37698  exanres  37767  iss2  37816  1cossres  37901  prtlem70  38329  fz1eqin  42189  fgraphopab  42631  rngcinvALTV  47338  ringcinvALTV  47372  itsclc0b  47845  i0oii  47938  io1ii  47939