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  1484  2eu4  2648  inrab  4279  uniin  4895  xpco  6262  dfpo2  6269  fin  6740  fndmin  7017  oaord  8511  nnaord  8583  ixpin  8896  isffth2  17880  fucinv  17938  setcinv  18052  rngcinv  20546  ringcinv  20580  unocv  21589  bldisj  24286  blin  24309  mbfmax  25550  mbfimaopnlem  25556  mbfaddlem  25561  i1faddlem  25594  i1fmullem  25595  lgsquadlem3  27293  numedglnl  29071  wlkeq  29562  ofpreima  32589  cntzun  33008  isunit2  33191  ordtconnlem1  33914  fneval  36340  mbfposadd  37661  anan  38217  exanres  38283  iss2  38326  1cossres  38420  prtlem70  38850  fz1eqin  42757  fgraphopab  43192  rngcinvALTV  48264  ringcinvALTV  48298  itsclc0b  48761  i0oii  48908  io1ii  48909  catcinv  49388