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

Theorem anandi 802
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 626 . . 3  |-  ( (
ph  /\  ph )  <->  ph )
21anbi1i 677 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
3 an4 798 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
42, 3bitr3i 243 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  inrab  3549  uniin  3970  xpco  5347  fin  5556  fndmin  5769  ndmovdistr  6168  oaord  6719  nnaord  6791  ixpin  7016  isffth2  14033  fucinv  14090  setcinv  14165  unocv  16823  bldisj  18322  blin  18337  mbfmax  19401  mbfimaopnlem  19407  mbfaddlem  19412  i1faddlem  19445  i1fmullem  19446  lgsquadlem3  21000  dfpo2  25129  fneval  26051  prtlem70  26382  fz1eqin  26511  fgraphopab  27191
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 178  df-an 361
  Copyright terms: Public domain W3C validator