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  2654  inrab  4291  uniin  4907  xpco  6278  dfpo2  6285  fin  6758  fndmin  7035  wfrlem5OLD  8327  oaord  8559  nnaord  8631  ixpin  8937  isffth2  17931  fucinv  17989  setcinv  18103  rngcinv  20597  ringcinv  20631  unocv  21640  bldisj  24337  blin  24360  mbfmax  25602  mbfimaopnlem  25608  mbfaddlem  25613  i1faddlem  25646  i1fmullem  25647  lgsquadlem3  27345  numedglnl  29123  wlkeq  29614  ofpreima  32643  cntzun  33062  isunit2  33235  ordtconnlem1  33955  fneval  36370  mbfposadd  37691  anan  38247  exanres  38313  iss2  38362  1cossres  38447  prtlem70  38875  fz1eqin  42792  fgraphopab  43227  rngcinvALTV  48251  ringcinvALTV  48285  itsclc0b  48752  i0oii  48894  io1ii  48895