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

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

Proof of Theorem anandi
StepHypRef Expression
1 anidm 554 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 610 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 635 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
42, 3bitr3i 266 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382
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 197  df-an 383
This theorem is referenced by:  anandi3  1091  an3andi  1593  2eu4  2705  inrab  4047  uniin  4595  xpco  5818  fin  6226  fndmin  6469  oaord  7785  nnaord  7857  ixpin  8091  isffth2  16783  fucinv  16840  setcinv  16947  unocv  20241  bldisj  22423  blin  22446  mbfmax  23636  mbfimaopnlem  23642  mbfaddlem  23647  i1faddlem  23680  i1fmullem  23681  lgsquadlem3  25328  numedglnl  26261  wlkeq  26764  ofpreima  29805  ordtconnlem1  30310  dfpo2  31983  fneval  32684  mbfposadd  33788  anan  34342  exanres  34404  iss2  34452  1cossres  34524  prtlem70  34662  fz1eqin  37856  fgraphopab  38312  rngcinv  42504  rngcinvALTV  42516  ringcinv  42555  ringcinvALTV  42579
  Copyright terms: Public domain W3C validator