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  4269  uniin  4885  xpco  6241  dfpo2  6248  fin  6708  fndmin  6983  oaord  8472  nnaord  8544  ixpin  8857  isffth2  17843  fucinv  17901  setcinv  18015  rngcinv  20540  ringcinv  20574  unocv  21605  bldisj  24302  blin  24325  mbfmax  25566  mbfimaopnlem  25572  mbfaddlem  25577  i1faddlem  25610  i1fmullem  25611  lgsquadlem3  27309  numedglnl  29107  wlkeq  29597  ofpreima  32622  cntzun  33034  isunit2  33190  ordtconnlem1  33890  fneval  36325  mbfposadd  37646  anan  38202  exanres  38268  iss2  38311  1cossres  38405  prtlem70  38835  fz1eqin  42742  fgraphopab  43176  rngcinvALTV  48261  ringcinvALTV  48295  itsclc0b  48758  i0oii  48905  io1ii  48906  catcinv  49385