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

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

Proof of Theorem anandi
StepHypRef Expression
1 anidm 546 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 602 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 627 . 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  1090  an3andi  1592  2eu4  2704  inrab  4045  uniin  4592  xpco  5819  fin  6225  fndmin  6467  oaord  7780  nnaord  7852  ixpin  8086  isffth2  16782  fucinv  16839  setcinv  16946  unocv  20240  bldisj  22422  blin  22445  mbfmax  23635  mbfimaopnlem  23641  mbfaddlem  23646  i1faddlem  23679  i1fmullem  23680  lgsquadlem3  25327  numedglnl  26260  wlkeq  26763  ofpreima  29799  ordtconnlem1  30304  dfpo2  31977  fneval  32678  mbfposadd  33782  anan  34337  exanres  34399  iss2  34447  1cossres  34519  prtlem70  34657  fz1eqin  37851  fgraphopab  38307  rngcinv  42499  rngcinvALTV  42511  ringcinv  42550  ringcinvALTV  42574
 Copyright terms: Public domain W3C validator