Theorem anandi 674

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anandi3  1098  an3andi  1478  2eu4  2740  inrab  4278  uniin  4865  xpco  6143  fin  6562  fndmin  6818  wfrlem5  7962  oaord  8176  nnaord  8248  ixpin  8490  isffth2  17189  fucinv  17246  setcinv  17353  unocv  20827  bldisj  23011  blin  23034  mbfmax  24253  mbfimaopnlem  24259  mbfaddlem  24264  i1faddlem  24297  i1fmullem  24298  lgsquadlem3  25961  numedglnl  26932  wlkeq  27418  ofpreima  30413  cntzun  30699  ordtconnlem1  31171  dfpo2  32995  fneval  33704  mbfposadd  34943  anan  35503  exanres  35556  iss2  35605  1cossres  35678  prtlem70  35997  fz1eqin  39372  fgraphopab  39816  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  ringcinvALTV  44334  itsclc0b  44766