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 568 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 627 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 656 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
42, 3bitr3i 280 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
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  1104  an3andi  1484  2eu4  2655  inrab  4226  uniin  4850  xpco  6157  fin  6604  fndmin  6870  wfrlem5  8064  oaord  8280  nnaord  8352  ixpin  8609  isffth2  17428  fucinv  17487  setcinv  17601  unocv  20647  bldisj  23301  blin  23324  mbfmax  24551  mbfimaopnlem  24557  mbfaddlem  24562  i1faddlem  24595  i1fmullem  24596  lgsquadlem3  26268  numedglnl  27240  wlkeq  27726  ofpreima  30727  cntzun  31044  ordtconnlem1  31593  dfpo2  33446  fneval  34283  mbfposadd  35566  anan  36121  exanres  36172  iss2  36221  1cossres  36294  prtlem70  36613  fz1eqin  40302  fgraphopab  40746  rngcinv  45220  rngcinvALTV  45232  ringcinv  45271  ringcinvALTV  45295  itsclc0b  45799  i0oii  45894  io1ii  45895
  Copyright terms: Public domain W3C validator