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  2650  inrab  4266  uniin  4883  xpco  6236  dfpo2  6243  fin  6703  fndmin  6978  oaord  8462  nnaord  8534  ixpin  8847  isffth2  17822  fucinv  17880  setcinv  17994  rngcinv  20550  ringcinv  20584  unocv  21615  bldisj  24311  blin  24334  mbfmax  25575  mbfimaopnlem  25581  mbfaddlem  25586  i1faddlem  25619  i1fmullem  25620  lgsquadlem3  27318  numedglnl  29120  wlkeq  29610  ofpreima  32642  cntzun  33043  isunit2  33202  ordtconnlem1  33932  fneval  36385  mbfposadd  37706  anan  38262  exanres  38328  iss2  38371  1cossres  38465  prtlem70  38895  fz1eqin  42801  fgraphopab  43235  rngcinvALTV  48306  ringcinvALTV  48340  itsclc0b  48803  i0oii  48950  io1ii  48951  catcinv  49430