Theorem anandi 686

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 572	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 633	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 666	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 279	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anandi3  1113  an3andi  1502  2eu4  2680  inrab  4268  uniinOLD  4889  xpco  6272  dfpo2  6279  fin  6740  fndmin  7022  oaord  8511  nnaord  8584  ixpin  8901  isffth2  17934  fucinv  17992  setcinv  18106  rngcinv  20666  ringcinv  20700  unocv  21712  bldisj  24438  blin  24461  mbfmax  25691  mbfimaopnlem  25697  mbfaddlem  25702  i1faddlem  25735  i1fmullem  25736  lgsquadlem3  27423  numedglnl  29291  wlkeq  29780  ofpreima  32817  cntzun  33220  isunit2  33381  ordtconnlem1  34182  fneval  36676  mbfposadd  38130  anan  38698  exanres  38764  iss2  38807  1cossres  38982  prtlem70  39445  fz1eqin  43314  fgraphopab  43744  rngcinvALTV  48862  ringcinvALTV  48896  itsclc0b  49358  i0oii  49505  io1ii  49506  catcinv  49984