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  1514  2eu4  2682  inrab  4264  uniinOLD  4895  xpco  6310  dfpo2  6317  fin  6784  fndmin  7067  oaord  8583  nnaord  8656  ixpin  8979  isffth2  18122  fucinv  18180  setcinv  18294  rngcinv  20919  ringcinv  20953  unocv  22016  bldisj  24747  blin  24770  mbfmax  26000  mbfimaopnlem  26006  mbfaddlem  26011  i1faddlem  26044  i1fmullem  26045  lgsquadlem3  27739  numedglnl  29752  wlkeq  30244  ofpreima  33331  cntzun  33710  isunit2  33870  ordtconnlem1  34626  fneval  37318  mbfposadd  38777  anan  39359  exanres  39425  iss2  39468  1cossres  39643  prtlem70  40106  fz1eqin  43973  fgraphopab  44397  rngcinvALTV  49578  ringcinvALTV  49612  itsclc0b  50089  i0oii  50239  io1ii  50240  catcinv  50739