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

Theorem anandi 835
Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
Assertion
Ref Expression
anandi  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )

Proof of Theorem anandi
StepHypRef Expression
1 anidm 648 . . 3  |-  ( (
ph  /\  ph )  <->  ph )
21anbi1i 699 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
3 an4 831 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
42, 3bitr3i 254 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  anandi3  996  an3andi  1377  2eu4  2354  inrab  3745  uniin  4236  xpco  5391  fin  5776  fndmin  6000  oaord  7252  nnaord  7324  ixpin  7551  isffth2  15808  fucinv  15865  setcinv  15972  unocv  19229  bldisj  21399  blin  21422  mbfmax  22591  mbfimaopnlem  22597  mbfaddlem  22602  i1faddlem  22637  i1fmullem  22638  lgsquadlem3  24270  2wlkeq  25420  ofpreima  28257  ordtconlem1  28725  dfpo2  30389  fneval  31000  mbfposadd  31901  prtlem70  32340  fz1eqin  35529  fgraphopab  36006  rngcinv  39254  rngcinvALTV  39266  ringcinv  39305  ringcinvALTV  39329
  Copyright terms: Public domain W3C validator