Theorem anandi 688

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 574	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 635	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 668	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 280	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anandi3  1117  an3andi  1506  2eu4  2684  inrab  4271  uniinOLD  4893  xpco  6280  dfpo2  6287  fin  6748  fndmin  7030  oaord  8520  nnaord  8593  ixpin  8909  isffth2  17965  fucinv  18023  setcinv  18137  rngcinv  20713  ringcinv  20747  unocv  21790  bldisj  24516  blin  24539  mbfmax  25769  mbfimaopnlem  25775  mbfaddlem  25780  i1faddlem  25813  i1fmullem  25814  lgsquadlem3  27504  numedglnl  29403  wlkeq  29892  ofpreima  32922  cntzun  33312  isunit2  33472  ordtconnlem1  34231  fneval  36725  mbfposadd  38178  anan  38746  exanres  38812  iss2  38855  1cossres  39030  prtlem70  39493  fz1eqin  43362  fgraphopab  43792  rngcinvALTV  48896  ringcinvALTV  48930  itsclc0b  49403  i0oii  49549  io1ii  49550  catcinv  50028