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  2655  inrab  4268  uniin  4887  xpco  6247  dfpo2  6254  fin  6714  fndmin  6990  oaord  8474  nnaord  8547  ixpin  8861  isffth2  17842  fucinv  17900  setcinv  18014  rngcinv  20570  ringcinv  20604  unocv  21635  bldisj  24342  blin  24365  mbfmax  25606  mbfimaopnlem  25612  mbfaddlem  25617  i1faddlem  25650  i1fmullem  25651  lgsquadlem3  27349  numedglnl  29217  wlkeq  29707  ofpreima  32743  cntzun  33161  isunit2  33322  ordtconnlem1  34081  fneval  36546  mbfposadd  37864  anan  38427  exanres  38490  iss2  38533  1cossres  38688  prtlem70  39113  fz1eqin  43007  fgraphopab  43441  rngcinvALTV  48518  ringcinvALTV  48552  itsclc0b  49014  i0oii  49161  io1ii  49162  catcinv  49640