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  2679  inrab  4261  uniinOLD  4891  xpco  6292  dfpo2  6299  fin  6762  fndmin  7044  oaord  8558  nnaord  8631  ixpin  8954  isffth2  18098  fucinv  18156  setcinv  18270  rngcinv  20894  ringcinv  20928  unocv  21991  bldisj  24722  blin  24745  mbfmax  25975  mbfimaopnlem  25981  mbfaddlem  25986  i1faddlem  26019  i1fmullem  26020  lgsquadlem3  27714  numedglnl  29727  wlkeq  30219  ofpreima  33306  cntzun  33686  isunit2  33846  ordtconnlem1  34602  fneval  37232  mbfposadd  38678  anan  39260  exanres  39326  iss2  39369  1cossres  39544  prtlem70  40007  fz1eqin  43873  fgraphopab  44298  rngcinvALTV  49466  ringcinvALTV  49500  itsclc0b  49977  i0oii  50127  io1ii  50128  catcinv  50627