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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  anandi3  1103  an3andi  1483  2eu4  2651  inrab  4307  uniin  4936  xpco  6289  dfpo2  6296  fin  6772  fndmin  7047  wfrlem5OLD  8313  oaord  8547  nnaord  8619  ixpin  8917  isffth2  17867  fucinv  17926  setcinv  18040  df2idl2  20860  unocv  21233  bldisj  23904  blin  23927  mbfmax  25166  mbfimaopnlem  25172  mbfaddlem  25177  i1faddlem  25210  i1fmullem  25211  lgsquadlem3  26885  numedglnl  28404  wlkeq  28891  ofpreima  31890  cntzun  32212  ordtconnlem1  32904  fneval  35237  mbfposadd  36535  anan  37093  exanres  37164  iss2  37213  1cossres  37299  prtlem70  37727  fz1eqin  41507  fgraphopab  41952  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  itsclc0b  47458  i0oii  47552  io1ii  47553