Theorem anandi 674

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 565	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 624	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 654	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 276	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anandi3  1102  an3andi  1482  2eu4  2649  inrab  4271  uniin  4897  xpco  6246  dfpo2  6253  fin  6727  fndmin  7000  wfrlem5OLD  8264  oaord  8499  nnaord  8571  ixpin  8868  isffth2  17817  fucinv  17876  setcinv  17990  unocv  21121  bldisj  23788  blin  23811  mbfmax  25050  mbfimaopnlem  25056  mbfaddlem  25061  i1faddlem  25094  i1fmullem  25095  lgsquadlem3  26767  numedglnl  28158  wlkeq  28645  ofpreima  31648  cntzun  31972  ordtconnlem1  32594  fneval  34900  mbfposadd  36198  anan  36757  exanres  36829  iss2  36878  1cossres  36964  prtlem70  37392  fz1eqin  41150  fgraphopab  41595  rngcinv  46399  rngcinvALTV  46411  ringcinv  46450  ringcinvALTV  46474  itsclc0b  46978  i0oii  47072  io1ii  47073