Theorem anandi 673

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

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

This theorem is referenced by:  anandi3  1101  an3andi  1481  2eu4  2656  inrab  4240  uniin  4865  xpco  6192  dfpo2  6199  fin  6654  fndmin  6922  wfrlem5OLD  8144  oaord  8378  nnaord  8450  ixpin  8711  isffth2  17632  fucinv  17691  setcinv  17805  unocv  20885  bldisj  23551  blin  23574  mbfmax  24813  mbfimaopnlem  24819  mbfaddlem  24824  i1faddlem  24857  i1fmullem  24858  lgsquadlem3  26530  numedglnl  27514  wlkeq  28001  ofpreima  31002  cntzun  31320  ordtconnlem1  31874  fneval  34541  mbfposadd  35824  anan  36379  exanres  36430  iss2  36479  1cossres  36552  prtlem70  36871  fz1eqin  40591  fgraphopab  41035  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  ringcinvALTV  45614  itsclc0b  46118  i0oii  46213  io1ii  46214