Theorem anandi 675

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 623	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 655	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 277	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anandi3  1100  an3andi  1479  2eu4  2646  inrab  4307  uniin  4934  xpco  6293  dfpo2  6300  fin  6777  fndmin  7054  wfrlem5OLD  8334  oaord  8568  nnaord  8640  ixpin  8942  isffth2  17905  fucinv  17965  setcinv  18079  rngcinv  20570  ringcinv  20604  unocv  21612  bldisj  24317  blin  24340  mbfmax  25591  mbfimaopnlem  25597  mbfaddlem  25602  i1faddlem  25635  i1fmullem  25636  lgsquadlem3  27328  numedglnl  28970  wlkeq  29461  ofpreima  32464  cntzun  32787  ordtconnlem1  33525  fneval  35836  mbfposadd  37140  anan  37698  exanres  37767  iss2  37816  1cossres  37901  prtlem70  38329  fz1eqin  42189  fgraphopab  42631  rngcinvALTV  47338  ringcinvALTV  47372  itsclc0b  47845  i0oii  47938  io1ii  47939

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »