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

Theorem anass 633
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
anass  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )

Proof of Theorem anass
StepHypRef Expression
1 id 21 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ph  /\  ( ps  /\  ch ) ) )
21anassrs 632 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ph  /\  ( ps  /\  ch ) ) )
3 id 21 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ( ph  /\  ps )  /\  ch )
)
43anasss 631 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ( ph  /\  ps )  /\  ch )
)
52, 4impbii 182 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  an12  775  an32  776  an13  777  an31  778  an4  800  3anass  943  4exdistr  2045  2sb5  2075  2sb5rf  2080  sbel2x  2088  r2exf  2550  r19.41  2663  ceqsex3v  2777  ceqsrex2v  2854  rexrab  2880  rexrab2  2884  rexss  3182  inass  3321  indifdir  3367  difin2  3372  difrab  3384  reupick3  3395  inssdif0  3463  rexdifsn  3694  eqvinop  4188  copsexg  4189  wefrc  4324  uniuni  4464  reusv2lem4  4475  reusv2  4477  reuxfr2d  4494  rabxp  4678  elvvv  4702  resopab2  4952  ssrnres  5069  elxp4  5112  elxp5  5113  cnvresima  5114  mptpreima  5118  coass  5143  imadif  5230  dff1o2  5380  eqfnfv3  5523  rexsupp  5549  isoini  5734  f1oiso  5747  oprabid  5781  dfoprab2  5794  mpt2eq123  5806  mpt2mptx  5837  resoprab2  5840  oprabex3  5861  ov3  5883  difxp  6052  frxp  6124  brtpos2  6139  oeeui  6533  oeeu  6534  omabs  6578  mapsnen  6871  xpsnen  6879  xpcomco  6885  xpassen  6889  wemapso2lem  7198  epfrs  7346  bnd2  7496  aceq1  7677  dfac5lem1  7683  dfac5lem2  7684  dfac5lem5  7687  kmlem3  7711  kmlem14  7722  pwfseqlem1  8213  ltexpi  8459  ltexprlem4  8596  axaddf  8700  axmulf  8701  rexuz  10201  rexuz2  10202  nnwos  10218  zmin  10244  rexrp  10305  elixx3g  10600  elfz2  10720  fzind2  10854  hashbclem  11320  resqrex  11666  rlim  11899  divalglem10  12528  divalgb  12530  gcdass  12651  isprm2  12693  infpn2  12887  ispos2  14009  issubg3  14564  resscntz  14734  subgdmdprd  15196  dprd2d2  15206  dfrhm2  15425  isassa  15983  aspval2  16013  istps2OLD  16586  istps3OLD  16587  ntreq0  16741  cmpcov2  17044  llyi  17127  nllyi  17128  subislly  17134  ptpjpre1  17193  tx1cn  17230  tx2cn  17231  txtube  17261  txkgen  17273  trfil2  17509  elflim2  17586  cnpflfi  17621  isfcls  17631  istlm  17794  blres  17904  metrest  17997  isnlm  18113  elcncf1di  18326  elpi1  18470  iscph  18533  itg1climres  18996  itgsubst  19323  ulmdvlem3  19706  cubic  20072  vmasum  20382  logfac2  20383  lgsquadlem1  20520  lgsquadlem2  20521  grpoidinvlem3  20798  h2hlm  21485  issh  21712  issh3  21724  ocsh  21787  cvbr2  22788  cvnbtwn2  22792  mdsl2i  22827  cvmdi  22829  mdsymlem2  22909  sumdmdii  22920  iscvm  23127  axacprim  23390  dfpo2  23448  dfdm5  23466  dfrn5  23467  preduz  23534  wfi  23541  frind  23577  sltval2  23643  dfon3  23773  brimg  23816  brsuccf  23820  dfrdg4  23828  tfrqfree  23829  axcontlem5  23936  ifscgr  24007  cgrxfr  24018  segcon2  24068  seglecgr12im  24073  segletr  24077  ellines  24115  eqvinopb  24296  copsexgb  24297  elo  24372  dfdir2  24623  cnvresimaOLD  25558  neifg  25652  isbnd2  25839  heibor1  25866  prtlem70  26047  prtlem100  26053  diophrex  26187  rmxdioph  26441  dford4  26454  islmodfg  26499  islssfg2  26501  isdomn3  26855  fgraphopab  26861  2sbc5g  26949  bnj250  27738  bnj251  27739  bnj256  27743  bnj168  27770  lsateln0  28315  islshpat  28337  lcvbr2  28342  lcvnbtwn2  28347  isopos  28500  cvrval2  28594  cvrnbtwn2  28595  ishlat2  28673  3dim0  28776  islvol5  28898  pmapjat1  29172  pclcmpatN  29220  pclfinclN  29269  cdlemefrs29pre00  29714  cdlemefrs29bpre0  29715  cdlemefrs29cpre1  29717  cdleme32a  29760  cdlemftr3  29884  dvhopellsm  30437  dibelval3  30467  diblsmopel  30491  mapdvalc  30949  mapdval4N  30952  mapdordlem1a  30954
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator