MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anandi Structured version   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  3605  uniin  4027  xpco  5406  fin  5615  fndmin  5829  ndmovdistr  6228  oaord  6782  nnaord  6854  ixpin  7079  isffth2  14105  fucinv  14162  setcinv  14237  unocv  16899  bldisj  18420  blin  18443  mbfmax  19533  mbfimaopnlem  19539  mbfaddlem  19544  i1faddlem  19577  i1fmullem  19578  lgsquadlem3  21132  ofpreima  24073  dfpo2  25370  mbfposadd  26244  fneval  26358  prtlem70  26689  fz1eqin  26818  fgraphopab  27497
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