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

Theorem anass 630
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 19 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ph  /\  ( ps  /\  ch ) ) )
21anassrs 629 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ph  /\  ( ps  /\  ch ) ) )
3 id 19 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ( ph  /\  ps )  /\  ch )
)
43anasss 628 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ( ph  /\  ps )  /\  ch )
)
52, 4impbii 180 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  an12  772  an32  773  an13  774  an31  775  an4  797  3anass  938  4exdistr  1854  2sb5  2053  2sb5rf  2058  sbel2x  2066  r2exf  2581  r19.41  2694  ceqsex3v  2828  ceqsrex2v  2905  rexrab  2931  rexrab2  2935  2reu5  2975  rexss  3242  inass  3381  indifdir  3427  difin2  3432  difrab  3444  reupick3  3455  inssdif0  3523  rexdifsn  3755  eqvinop  4253  copsexg  4254  wefrc  4389  uniuni  4529  reusv2lem4  4540  reusv2  4542  rabxp  4727  elvvv  4751  resopab2  5001  ssrnres  5118  elxp4  5162  elxp5  5163  cnvresima  5164  mptpreima  5168  coass  5193  imadif  5329  dff1o2  5479  eqfnfv3  5626  rexsupp  5652  isoini  5837  f1oiso  5850  oprabid  5884  dfoprab2  5897  mpt2eq123  5909  mpt2mptx  5940  resoprab2  5943  oprabex3  5964  ov3  5986  difxp  6155  frxp  6227  brtpos2  6242  oeeui  6602  oeeu  6603  omabs  6647  mapsnen  6940  xpsnen  6948  xpcomco  6954  xpassen  6958  wemapso2lem  7267  epfrs  7415  bnd2  7565  aceq1  7746  dfac5lem1  7752  dfac5lem2  7753  dfac5lem5  7756  kmlem3  7780  kmlem14  7791  pwfseqlem1  8282  ltexpi  8528  ltexprlem4  8665  axaddf  8769  axmulf  8770  rexuz  10271  rexuz2  10272  nnwos  10288  zmin  10314  rexrp  10375  elixx3g  10671  elfz2  10791  fzind2  10925  hashbclem  11392  resqrex  11738  rlim  11971  divalglem10  12603  divalgb  12605  gcdass  12726  isprm2  12768  infpn2  12962  ispos2  14084  issubg3  14639  resscntz  14809  subgdmdprd  15271  dprd2d2  15281  dfrhm2  15500  isassa  16058  aspval2  16088  istps2OLD  16661  istps3OLD  16662  ntreq0  16816  cmpcov2  17119  llyi  17202  nllyi  17203  subislly  17209  ptpjpre1  17268  tx1cn  17305  tx2cn  17306  txtube  17336  txkgen  17348  trfil2  17584  elflim2  17661  cnpflfi  17696  isfcls  17706  istlm  17869  blres  17979  metrest  18072  isnlm  18188  elcncf1di  18401  elpi1  18545  iscph  18608  itg1climres  19071  itgsubst  19398  ulmdvlem3  19781  cubic  20147  vmasum  20457  logfac2  20458  lgsquadlem1  20595  lgsquadlem2  20596  grpoidinvlem3  20875  h2hlm  21562  issh  21789  issh3  21801  ocsh  21864  cvbr2  22865  cvnbtwn2  22869  mdsl2i  22904  cvmdi  22906  mdsymlem2  22986  sumdmdii  22997  1stmbfm  23567  2ndmbfm  23568  iscvm  23792  axacprim  24055  dfpo2  24114  dfdm5  24134  dfrn5  24135  preduz  24202  wfi  24209  frind  24245  sltval2  24312  nofulllem5  24362  dfon3  24434  elfuns  24456  brimg  24478  brsuccf  24482  dfrdg4  24490  tfrqfree  24491  axcontlem5  24598  ifscgr  24669  cgrxfr  24680  segcon2  24730  seglecgr12im  24735  segletr  24739  ellines  24777  itg2addnc  24935  areacirclem6  24941  eqvinopb  24976  copsexgb  24977  elo  25052  dfdir2  25302  cnvresimaOLD  26237  neifg  26331  isbnd2  26518  heibor1  26545  prtlem70  26726  prtlem100  26732  diophrex  26866  rmxdioph  27120  dford4  27133  islmodfg  27178  islssfg2  27180  isdomn3  27534  fgraphopab  27540  2sbc5g  27627  1to2vfriswmgra  28195  bnj250  28799  bnj251  28800  bnj256  28804  bnj168  28831  lsateln0  29258  islshpat  29280  lcvbr2  29285  lcvnbtwn2  29290  isopos  29443  cvrval2  29537  cvrnbtwn2  29538  ishlat2  29616  3dim0  29719  islvol5  29841  pmapjat1  30115  pclcmpatN  30163  pclfinclN  30212  cdlemefrs29pre00  30657  cdlemefrs29bpre0  30658  cdlemefrs29cpre1  30660  cdleme32a  30703  cdlemftr3  30827  dvhopellsm  31380  dibelval3  31410  diblsmopel  31434  mapdvalc  31892  mapdval4N  31895  mapdordlem1a  31897
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