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

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

Proof of Theorem anandi
StepHypRef Expression
1 anidm 564 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 624 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 656 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
42, 3bitr3i 277 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
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  1102  an3andi  1484  2eu4  2655  inrab  4316  uniin  4931  xpco  6309  dfpo2  6316  fin  6788  fndmin  7065  wfrlem5OLD  8353  oaord  8585  nnaord  8657  ixpin  8963  isffth2  17963  fucinv  18021  setcinv  18135  rngcinv  20637  ringcinv  20671  unocv  21698  bldisj  24408  blin  24431  mbfmax  25684  mbfimaopnlem  25690  mbfaddlem  25695  i1faddlem  25728  i1fmullem  25729  lgsquadlem3  27426  numedglnl  29161  wlkeq  29652  ofpreima  32675  cntzun  33071  isunit2  33244  ordtconnlem1  33923  fneval  36353  mbfposadd  37674  anan  38230  exanres  38296  iss2  38345  1cossres  38430  prtlem70  38858  fz1eqin  42780  fgraphopab  43215  rngcinvALTV  48192  ringcinvALTV  48226  itsclc0b  48693  i0oii  48817  io1ii  48818
  Copyright terms: Public domain W3C validator