Theorem anandi 867

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 674	. . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
2	1	anbi1i 727	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		an4 861	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
4	2, 3	bitr3i 265	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anandi3  1045  an3andi  1437  2eu4  2544  inrab  3858  uniin  4393  xpco  5592  fin  5998  fndmin  6232  oaord  7514  nnaord  7586  ixpin  7819  isffth2  16399  fucinv  16456  setcinv  16563  unocv  19843  bldisj  22013  blin  22036  mbfmax  23222  mbfimaopnlem  23228  mbfaddlem  23233  i1faddlem  23266  i1fmullem  23267  lgsquadlem3  24907  2wlkeq  26235  ofpreima  28848  ordtconlem1  29298  dfpo2  30898  fneval  31517  mbfposadd  32627  prtlem70  33157  fz1eqin  36350  fgraphopab  36807  1wlkeq  40838  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848