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  3453  uniin  3863  fin  5437  fndmin  5648  ndmovdistr  6025  oaord  6561  nnaord  6633  ixpin  6857  isffth2  13806  fucinv  13863  setcinv  13938  unocv  16596  bldisj  17971  blin  17986  mbfmax  19020  mbfimaopnlem  19026  mbfaddlem  19031  i1faddlem  19064  i1fmullem  19065  lgsquadlem3  20611  dfpo2  24183  fneval  26390  prtlem70  26818  fz1eqin  26951  fgraphopab  27632
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