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  2681  inrab  4265  uniinOLD  4895  xpco  6291  dfpo2  6298  fin  6759  fndmin  7041  oaord  8538  nnaord  8611  ixpin  8934  isffth2  18013  fucinv  18071  setcinv  18185  rngcinv  20805  ringcinv  20839  unocv  21899  bldisj  24630  blin  24653  mbfmax  25883  mbfimaopnlem  25889  mbfaddlem  25894  i1faddlem  25927  i1fmullem  25928  lgsquadlem3  27626  numedglnl  29609  wlkeq  30101  ofpreima  33146  cntzun  33527  isunit2  33687  ordtconnlem1  34442  fneval  36979  mbfposadd  38424  anan  38991  exanres  39057  iss2  39100  1cossres  39275  prtlem70  39738  fz1eqin  43622  fgraphopab  44052  rngcinvALTV  49199  ringcinvALTV  49233  itsclc0b  49710  i0oii  49854  io1ii  49855  catcinv  50333