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  2554  r19.41  2667  ceqsex3v  2801  ceqsrex2v  2878  rexrab  2904  rexrab2  2908  2reu5  2948  rexss  3215  inass  3354  indifdir  3400  difin2  3405  difrab  3417  reupick3  3428  inssdif0  3496  rexdifsn  3728  eqvinop  4224  copsexg  4225  wefrc  4360  uniuni  4500  reusv2lem4  4511  reusv2  4513  rabxp  4698  elvvv  4722  resopab2  4972  ssrnres  5089  elxp4  5132  elxp5  5133  cnvresima  5134  mptpreima  5138  coass  5163  imadif  5266  dff1o2  5416  eqfnfv3  5559  rexsupp  5585  isoini  5770  f1oiso  5783  oprabid  5817  dfoprab2  5830  mpt2eq123  5842  mpt2mptx  5873  resoprab2  5876  oprabex3  5897  ov3  5919  difxp  6088  frxp  6160  brtpos2  6175  oeeui  6569  oeeu  6570  omabs  6614  mapsnen  6907  xpsnen  6915  xpcomco  6921  xpassen  6925  wemapso2lem  7234  epfrs  7382  bnd2  7532  aceq1  7713  dfac5lem1  7719  dfac5lem2  7720  dfac5lem5  7723  kmlem3  7747  kmlem14  7758  pwfseqlem1  8249  ltexpi  8495  ltexprlem4  8632  axaddf  8736  axmulf  8737  rexuz  10238  rexuz2  10239  nnwos  10255  zmin  10281  rexrp  10342  elixx3g  10637  elfz2  10757  fzind2  10891  hashbclem  11357  resqrex  11703  rlim  11936  divalglem10  12565  divalgb  12567  gcdass  12688  isprm2  12730  infpn2  12924  ispos2  14046  issubg3  14601  resscntz  14771  subgdmdprd  15233  dprd2d2  15243  dfrhm2  15462  isassa  16020  aspval2  16050  istps2OLD  16623  istps3OLD  16624  ntreq0  16778  cmpcov2  17081  llyi  17164  nllyi  17165  subislly  17171  ptpjpre1  17230  tx1cn  17267  tx2cn  17268  txtube  17298  txkgen  17310  trfil2  17546  elflim2  17623  cnpflfi  17658  isfcls  17668  istlm  17831  blres  17941  metrest  18034  isnlm  18150  elcncf1di  18363  elpi1  18507  iscph  18570  itg1climres  19033  itgsubst  19360  ulmdvlem3  19743  cubic  20109  vmasum  20419  logfac2  20420  lgsquadlem1  20557  lgsquadlem2  20558  grpoidinvlem3  20835  h2hlm  21522  issh  21749  issh3  21761  ocsh  21824  cvbr2  22825  cvnbtwn2  22829  mdsl2i  22864  cvmdi  22866  mdsymlem2  22946  sumdmdii  22957  iscvm  23164  axacprim  23427  dfpo2  23485  dfdm5  23503  dfrn5  23504  preduz  23571  wfi  23578  frind  23614  sltval2  23680  dfon3  23810  brimg  23853  brsuccf  23857  dfrdg4  23865  tfrqfree  23866  axcontlem5  23973  ifscgr  24044  cgrxfr  24055  segcon2  24105  seglecgr12im  24110  segletr  24114  ellines  24152  eqvinopb  24333  copsexgb  24334  elo  24409  dfdir2  24660  cnvresimaOLD  25595  neifg  25689  isbnd2  25876  heibor1  25903  prtlem70  26084  prtlem100  26090  diophrex  26224  rmxdioph  26478  dford4  26491  islmodfg  26536  islssfg2  26538  isdomn3  26892  fgraphopab  26898  2sbc5g  26986  bnj250  27867  bnj251  27868  bnj256  27872  bnj168  27899  lsateln0  28444  islshpat  28466  lcvbr2  28471  lcvnbtwn2  28476  isopos  28629  cvrval2  28723  cvrnbtwn2  28724  ishlat2  28802  3dim0  28905  islvol5  29027  pmapjat1  29301  pclcmpatN  29349  pclfinclN  29398  cdlemefrs29pre00  29843  cdlemefrs29bpre0  29844  cdlemefrs29cpre1  29846  cdleme32a  29889  cdlemftr3  30013  dvhopellsm  30566  dibelval3  30596  diblsmopel  30620  mapdvalc  31078  mapdval4N  31081  mapdordlem1a  31083
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