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

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

Proof of Theorem anandi
StepHypRef Expression
1 anidm 674 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 727 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 861 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
42, 3bitr3i 265 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  anandi3  1045  an3andi  1437  2eu4  2544  inrab  3858  uniin  4393  xpco  5592  fin  5998  fndmin  6232  oaord  7514  nnaord  7586  ixpin  7819  isffth2  16399  fucinv  16456  setcinv  16563  unocv  19843  bldisj  22013  blin  22036  mbfmax  23222  mbfimaopnlem  23228  mbfaddlem  23233  i1faddlem  23266  i1fmullem  23267  lgsquadlem3  24907  2wlkeq  26235  ofpreima  28848  ordtconlem1  29298  dfpo2  30898  fneval  31517  mbfposadd  32627  prtlem70  33157  fz1eqin  36350  fgraphopab  36807  1wlkeq  40838  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848
 Copyright terms: Public domain W3C validator