Theorem anandi 677

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 564	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 625	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 657	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 277	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anandi3  1102  an3andi  1485  2eu4  2656  inrab  4270  uniin  4889  xpco  6255  dfpo2  6262  fin  6722  fndmin  6999  oaord  8484  nnaord  8557  ixpin  8873  isffth2  17854  fucinv  17912  setcinv  18026  rngcinv  20582  ringcinv  20616  unocv  21647  bldisj  24354  blin  24377  mbfmax  25618  mbfimaopnlem  25624  mbfaddlem  25629  i1faddlem  25662  i1fmullem  25663  lgsquadlem3  27361  numedglnl  29229  wlkeq  29719  ofpreima  32754  cntzun  33172  isunit2  33333  ordtconnlem1  34101  fneval  36565  mbfposadd  37912  anan  38480  exanres  38546  iss2  38589  1cossres  38764  prtlem70  39227  fz1eqin  43120  fgraphopab  43554  rngcinvALTV  48630  ringcinvALTV  48664  itsclc0b  49126  i0oii  49273  io1ii  49274  catcinv  49752