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  1852  2sb5  2051  2sb5rf  2056  sbel2x  2064  r2exf  2579  r19.41  2692  ceqsex3v  2826  ceqsrex2v  2903  rexrab  2929  rexrab2  2933  2reu5  2973  rexss  3240  inass  3379  indifdir  3425  difin2  3430  difrab  3442  reupick3  3453  inssdif0  3521  rexdifsn  3753  eqvinop  4251  copsexg  4252  wefrc  4387  uniuni  4527  reusv2lem4  4538  reusv2  4540  rabxp  4725  elvvv  4749  resopab2  4999  ssrnres  5116  elxp4  5160  elxp5  5161  cnvresima  5162  mptpreima  5166  coass  5191  imadif  5327  dff1o2  5477  eqfnfv3  5624  rexsupp  5650  isoini  5835  f1oiso  5848  oprabid  5882  dfoprab2  5895  mpt2eq123  5907  mpt2mptx  5938  resoprab2  5941  oprabex3  5962  ov3  5984  difxp  6153  frxp  6225  brtpos2  6240  oeeui  6600  oeeu  6601  omabs  6645  mapsnen  6938  xpsnen  6946  xpcomco  6952  xpassen  6956  wemapso2lem  7265  epfrs  7413  bnd2  7563  aceq1  7744  dfac5lem1  7750  dfac5lem2  7751  dfac5lem5  7754  kmlem3  7778  kmlem14  7789  pwfseqlem1  8280  ltexpi  8526  ltexprlem4  8663  axaddf  8767  axmulf  8768  rexuz  10269  rexuz2  10270  nnwos  10286  zmin  10312  rexrp  10373  elixx3g  10669  elfz2  10789  fzind2  10923  hashbclem  11390  resqrex  11736  rlim  11969  divalglem10  12601  divalgb  12603  gcdass  12724  isprm2  12766  infpn2  12960  ispos2  14082  issubg3  14637  resscntz  14807  subgdmdprd  15269  dprd2d2  15279  dfrhm2  15498  isassa  16056  aspval2  16086  istps2OLD  16659  istps3OLD  16660  ntreq0  16814  cmpcov2  17117  llyi  17200  nllyi  17201  subislly  17207  ptpjpre1  17266  tx1cn  17303  tx2cn  17304  txtube  17334  txkgen  17346  trfil2  17582  elflim2  17659  cnpflfi  17694  isfcls  17704  istlm  17867  blres  17977  metrest  18070  isnlm  18186  elcncf1di  18399  elpi1  18543  iscph  18606  itg1climres  19069  itgsubst  19396  ulmdvlem3  19779  cubic  20145  vmasum  20455  logfac2  20456  lgsquadlem1  20593  lgsquadlem2  20594  grpoidinvlem3  20873  h2hlm  21560  issh  21787  issh3  21799  ocsh  21862  cvbr2  22863  cvnbtwn2  22867  mdsl2i  22902  cvmdi  22904  mdsymlem2  22984  sumdmdii  22995  1stmbfm  23565  2ndmbfm  23566  iscvm  23790  axacprim  24053  dfpo2  24112  dfdm5  24132  dfrn5  24133  preduz  24200  wfi  24207  frind  24243  sltval2  24310  nofulllem5  24360  dfon3  24432  elfuns  24454  brimg  24476  brsuccf  24480  dfrdg4  24488  tfrqfree  24489  axcontlem5  24596  ifscgr  24667  cgrxfr  24678  segcon2  24728  seglecgr12im  24733  segletr  24737  ellines  24775  areacirclem6  24930  eqvinopb  24965  copsexgb  24966  elo  25041  dfdir2  25291  cnvresimaOLD  26226  neifg  26320  isbnd2  26507  heibor1  26534  prtlem70  26715  prtlem100  26721  diophrex  26855  rmxdioph  27109  dford4  27122  islmodfg  27167  islssfg2  27169  isdomn3  27523  fgraphopab  27529  2sbc5g  27616  1to2vfriswmgra  28184  bnj250  28726  bnj251  28727  bnj256  28731  bnj168  28758  lsateln0  29185  islshpat  29207  lcvbr2  29212  lcvnbtwn2  29217  isopos  29370  cvrval2  29464  cvrnbtwn2  29465  ishlat2  29543  3dim0  29646  islvol5  29768  pmapjat1  30042  pclcmpatN  30090  pclfinclN  30139  cdlemefrs29pre00  30584  cdlemefrs29bpre0  30585  cdlemefrs29cpre1  30587  cdleme32a  30630  cdlemftr3  30754  dvhopellsm  31307  dibelval3  31337  diblsmopel  31361  mapdvalc  31819  mapdval4N  31822  mapdordlem1a  31824
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