Theorem anandi 675

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 623	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 655	. 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  1482  2eu4  2658  inrab  4335  uniin  4955  xpco  6320  dfpo2  6327  fin  6801  fndmin  7078  wfrlem5OLD  8369  oaord  8603  nnaord  8675  ixpin  8981  isffth2  17983  fucinv  18043  setcinv  18157  rngcinv  20659  ringcinv  20693  unocv  21721  bldisj  24429  blin  24452  mbfmax  25703  mbfimaopnlem  25709  mbfaddlem  25714  i1faddlem  25747  i1fmullem  25748  lgsquadlem3  27444  numedglnl  29179  wlkeq  29670  ofpreima  32683  cntzun  33044  isunit2  33220  ordtconnlem1  33870  fneval  36318  mbfposadd  37627  anan  38183  exanres  38251  iss2  38300  1cossres  38385  prtlem70  38813  fz1eqin  42725  fgraphopab  43164  rngcinvALTV  47999  ringcinvALTV  48033  itsclc0b  48506  i0oii  48599  io1ii  48600