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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anandi3  1099  an3andi  1479  2eu4  2716  inrab  4227  uniin  4824  xpco  6108  fin  6533  fndmin  6792  wfrlem5  7942  oaord  8156  nnaord  8228  ixpin  8470  isffth2  17178  fucinv  17235  setcinv  17342  unocv  20369  bldisj  23005  blin  23028  mbfmax  24253  mbfimaopnlem  24259  mbfaddlem  24264  i1faddlem  24297  i1fmullem  24298  lgsquadlem3  25966  numedglnl  26937  wlkeq  27423  ofpreima  30428  cntzun  30745  ordtconnlem1  31277  dfpo2  33104  fneval  33813  mbfposadd  35104  anan  35659  exanres  35712  iss2  35761  1cossres  35834  prtlem70  36153  fz1eqin  39710  fgraphopab  40154  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680  itsclc0b  45186