Theorem anandi 676

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 624	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 656	. 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  1101  an3andi  1481  2eu4  2652  inrab  4321  uniin  4935  xpco  6310  dfpo2  6317  fin  6788  fndmin  7064  wfrlem5OLD  8351  oaord  8583  nnaord  8655  ixpin  8961  isffth2  17969  fucinv  18029  setcinv  18143  rngcinv  20653  ringcinv  20687  unocv  21715  bldisj  24423  blin  24446  mbfmax  25697  mbfimaopnlem  25703  mbfaddlem  25708  i1faddlem  25741  i1fmullem  25742  lgsquadlem3  27440  numedglnl  29175  wlkeq  29666  ofpreima  32681  cntzun  33053  isunit2  33229  ordtconnlem1  33884  fneval  36334  mbfposadd  37653  anan  38209  exanres  38276  iss2  38325  1cossres  38410  prtlem70  38838  fz1eqin  42756  fgraphopab  43191  rngcinvALTV  48119  ringcinvALTV  48153  itsclc0b  48621  i0oii  48715  io1ii  48716