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

Theorem anandi 824
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 644 . . 3  |-  ( (
ph  /\  ph )  <->  ph )
21anbi1i 695 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
3 an4 820 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
42, 3bitr3i 251 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  anandi3  979  an3andi  1331  2eu4  2368  inrab  3622  uniin  4111  xpco  5377  fin  5591  fndmin  5810  oaord  6986  nnaord  7058  ixpin  7288  isffth2  14826  fucinv  14883  setcinv  14958  unocv  18105  bldisj  19973  blin  19996  mbfmax  21127  mbfimaopnlem  21133  mbfaddlem  21138  i1faddlem  21171  i1fmullem  21172  lgsquadlem3  22695  ofpreima  25984  ordtconlem1  26354  dfpo2  27565  mbfposadd  28439  fneval  28559  prtlem70  28996  fz1eqin  29107  fgraphopab  29578  2wlkeq  30288
  Copyright terms: Public domain W3C validator