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

Theorem anandi 836
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 649 . . 3  |-  ( (
ph  /\  ph )  <->  ph )
21anbi1i 700 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
3 an4 832 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
42, 3bitr3i 255 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  anandi3  998  an3andi  1381  2eu4  2384  inrab  3714  uniin  4217  xpco  5375  fin  5761  fndmin  5987  oaord  7245  nnaord  7317  ixpin  7544  isffth2  15814  fucinv  15871  setcinv  15978  unocv  19236  bldisj  21406  blin  21429  mbfmax  22598  mbfimaopnlem  22604  mbfaddlem  22609  i1faddlem  22644  i1fmullem  22645  lgsquadlem3  24277  2wlkeq  25428  ofpreima  28261  ordtconlem1  28723  dfpo2  30388  fneval  31001  mbfposadd  31981  prtlem70  32419  fz1eqin  35605  fgraphopab  36081  rngcinv  39970  rngcinvALTV  39982  ringcinv  40021  ringcinvALTV  40045
  Copyright terms: Public domain W3C validator