MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anandi Structured version   Visualization version   GIF version

Theorem anandi 867
Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
Assertion
Ref Expression
anandi ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))

Proof of Theorem anandi
StepHypRef Expression
1 anidm 674 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 727 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 861 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
42, 3bitr3i 265 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
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  4388  xpco  5578  fin  5983  fndmin  6217  oaord  7492  nnaord  7564  ixpin  7797  isffth2  16348  fucinv  16405  setcinv  16512  unocv  19791  bldisj  21961  blin  21984  mbfmax  23167  mbfimaopnlem  23173  mbfaddlem  23178  i1faddlem  23211  i1fmullem  23212  lgsquadlem3  24852  2wlkeq  26029  ofpreima  28642  ordtconlem1  29092  dfpo2  30692  fneval  31311  mbfposadd  32421  prtlem70  32951  fz1eqin  36144  fgraphopab  36601  1wlkeq  40830  rngcinv  41765  rngcinvALTV  41777  ringcinv  41816  ringcinvALTV  41840
  Copyright terms: Public domain W3C validator