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  4257  uniin  4875  xpco  6247  dfpo2  6254  fin  6714  fndmin  6991  oaord  8475  nnaord  8548  ixpin  8864  isffth2  17876  fucinv  17934  setcinv  18048  rngcinv  20605  ringcinv  20639  unocv  21670  bldisj  24373  blin  24396  mbfmax  25626  mbfimaopnlem  25632  mbfaddlem  25637  i1faddlem  25670  i1fmullem  25671  lgsquadlem3  27359  numedglnl  29227  wlkeq  29717  ofpreima  32753  cntzun  33155  isunit2  33316  ordtconnlem1  34084  fneval  36550  mbfposadd  38002  anan  38570  exanres  38636  iss2  38679  1cossres  38854  prtlem70  39317  fz1eqin  43215  fgraphopab  43649  rngcinvALTV  48764  ringcinvALTV  48798  itsclc0b  49260  i0oii  49407  io1ii  49408  catcinv  49886