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

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

Proof of Theorem anandi
StepHypRef Expression
1 anidm 565 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 623 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 652 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
42, 3bitr3i 278 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  anandi3  1096  an3andi  1475  2eu4  2738  inrab  4278  uniin  4856  xpco  6137  fin  6555  fndmin  6810  wfrlem5  7953  oaord  8166  nnaord  8238  ixpin  8479  isffth2  17178  fucinv  17235  setcinv  17342  unocv  20740  bldisj  22923  blin  22946  mbfmax  24165  mbfimaopnlem  24171  mbfaddlem  24176  i1faddlem  24209  i1fmullem  24210  lgsquadlem3  25872  numedglnl  26844  wlkeq  27330  ofpreima  30326  cntzun  30610  ordtconnlem1  31054  dfpo2  32876  fneval  33585  mbfposadd  34807  anan  35368  exanres  35421  iss2  35470  1cossres  35542  prtlem70  35861  fz1eqin  39228  fgraphopab  39672  rngcinv  44081  rngcinvALTV  44093  ringcinv  44132  ringcinvALTV  44156  itsclc0b  44588
  Copyright terms: Public domain W3C validator