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  28435  wlkeq  28922  ofpreima  31921  cntzun  32243  ordtconnlem1  32935  fneval  35285  mbfposadd  36583  anan  37141  exanres  37212  iss2  37261  1cossres  37347  prtlem70  37775  fz1eqin  41555  fgraphopab  42000  rngcinv  46927  rngcinvALTV  46939  ringcinv  46978  ringcinvALTV  47002  itsclc0b  47506  i0oii  47600  io1ii  47601