Theorem anandi 689

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 575	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 636	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 669	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 280	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anandi3  1119  an3andi  1513  2eu4  2685  inrab  4272  uniinOLD  4902  xpco  6297  dfpo2  6304  fin  6765  fndmin  7047  oaord  8541  nnaord  8614  ixpin  8930  isffth2  18000  fucinv  18058  setcinv  18172  rngcinv  20773  ringcinv  20807  unocv  21867  bldisj  24592  blin  24615  mbfmax  25845  mbfimaopnlem  25851  mbfaddlem  25856  i1faddlem  25889  i1fmullem  25890  lgsquadlem3  27583  numedglnl  29531  wlkeq  30020  ofpreima  33047  cntzun  33430  isunit2  33590  ordtconnlem1  34345  fneval  36903  mbfposadd  38358  anan  38924  exanres  38990  iss2  39033  1cossres  39208  prtlem70  39671  fz1eqin  43540  fgraphopab  43970  rngcinvALTV  49081  ringcinvALTV  49115  itsclc0b  49592  i0oii  49738  io1ii  49739  catcinv  50217