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

Theorem anandi 801
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 625 . . 3  |-  ( (
ph  /\  ph )  <->  ph )
21anbi1i 676 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
3 an4 797 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
42, 3bitr3i 242 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  inrab  3440  uniin  3847  fin  5421  fndmin  5632  ndmovdistr  6009  oaord  6545  nnaord  6617  ixpin  6841  isffth2  13790  fucinv  13847  setcinv  13922  unocv  16580  bldisj  17955  blin  17970  mbfmax  19004  mbfimaopnlem  19010  mbfaddlem  19015  i1faddlem  19048  i1fmullem  19049  lgsquadlem3  20595  dfpo2  24112  fneval  26287  prtlem70  26715  fz1eqin  26848  fgraphopab  27529
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator