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  2652  inrab  4265  uniin  4882  xpco  6241  dfpo2  6248  fin  6708  fndmin  6984  oaord  8468  nnaord  8540  ixpin  8853  isffth2  17827  fucinv  17885  setcinv  17999  rngcinv  20554  ringcinv  20588  unocv  21619  bldisj  24314  blin  24337  mbfmax  25578  mbfimaopnlem  25584  mbfaddlem  25589  i1faddlem  25622  i1fmullem  25623  lgsquadlem3  27321  numedglnl  29124  wlkeq  29614  ofpreima  32649  cntzun  33055  isunit2  33214  ordtconnlem1  33958  fneval  36417  mbfposadd  37727  anan  38290  exanres  38353  iss2  38396  1cossres  38551  prtlem70  38976  fz1eqin  42886  fgraphopab  43320  rngcinvALTV  48400  ringcinvALTV  48434  itsclc0b  48897  i0oii  49044  io1ii  49045  catcinv  49524