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  2044  2sb5  2072  2sb5rf  2077  sbel2x  2085  r2exf  2541  r19.41  2654  ceqsex3v  2764  ceqsrex2v  2840  rexrab  2866  rexrab2  2870  rexss  3161  inass  3286  indifdir  3332  difin2  3337  difrab  3349  reupick3  3360  inssdif0  3427  rexdifsn  3655  eqvinop  4144  copsexg  4145  wefrc  4280  uniuni  4418  reusv2lem4  4429  reusv2  4431  reuxfr2d  4448  rabxp  4632  elvvv  4656  resopab2  4906  ssrnres  5023  elxp4  5066  elxp5  5067  cnvresima  5068  mptpreima  5072  coass  5097  imadif  5184  dff1o2  5334  eqfnfv3  5476  rexsupp  5502  isoini  5687  f1oiso  5700  oprabid  5734  dfoprab2  5747  mpt2eq123  5759  mpt2mptx  5790  resoprab2  5793  oprabex3  5814  ov3  5836  difxp  6005  frxp  6077  brtpos2  6092  oeeui  6486  oeeu  6487  omabs  6531  mapsnen  6823  xpsnen  6831  xpcomco  6837  xpassen  6841  wemapso2lem  7149  epfrs  7297  bnd2  7447  aceq1  7628  dfac5lem1  7634  dfac5lem2  7635  dfac5lem5  7638  kmlem3  7662  kmlem14  7673  pwfseqlem1  8160  ltexpi  8406  ltexprlem4  8543  axaddf  8647  axmulf  8648  rexuz  10148  rexuz2  10149  nnwos  10165  zmin  10191  rexrp  10252  elixx3g  10547  elfz2  10667  fzind2  10801  hashbclem  11267  resqrex  11613  rlim  11846  divalglem10  12475  divalgb  12477  gcdass  12598  isprm2  12640  infpn2  12834  ispos2  13926  issubg3  14472  resscntz  14642  subgdmdprd  15104  dprd2d2  15114  dfrhm2  15333  isassa  15888  aspval2  15918  istps2OLD  16491  istps3OLD  16492  ntreq0  16646  cmpcov2  16949  llyi  17032  nllyi  17033  subislly  17039  ptpjpre1  17098  tx1cn  17135  tx2cn  17136  txtube  17166  txkgen  17178  trfil2  17414  elflim2  17491  cnpflfi  17526  isfcls  17536  istlm  17699  blres  17809  metrest  17902  isnlm  18018  elcncf1di  18231  elpi1  18375  iscph  18438  itg1climres  18901  itgsubst  19228  ulmdvlem3  19611  cubic  19977  vmasum  20287  logfac2  20288  lgsquadlem1  20425  lgsquadlem2  20426  grpoidinvlem3  20703  h2hlm  21390  issh  21617  issh3  21629  ocsh  21692  cvbr2  22693  cvnbtwn2  22697  mdsl2i  22732  cvmdi  22734  mdsymlem2  22814  sumdmdii  22825  iscvm  22961  axacprim  23224  dfpo2  23282  dfdm5  23300  dfrn5  23301  preduz  23368  wfi  23375  frind  23411  sltval2  23477  dfon3  23607  brimg  23650  brsuccf  23654  dfrdg4  23662  tfrqfree  23663  axcontlem5  23770  ifscgr  23841  cgrxfr  23852  segcon2  23902  seglecgr12im  23907  segletr  23911  ellines  23949  eqvinopb  24130  copsexgb  24131  elo  24206  dfdir2  24457  cnvresimaOLD  25392  neifg  25486  isbnd2  25673  heibor1  25700  prtlem70  25881  prtlem100  25887  diophrex  26021  rmxdioph  26275  dford4  26288  islmodfg  26333  islssfg2  26335  isdomn3  26689  fgraphopab  26695  2sbc5g  26783  bnj250  27415  bnj251  27416  bnj256  27420  bnj168  27447  lsateln0  27874  islshpat  27896  lcvbr2  27901  lcvnbtwn2  27906  isopos  28059  cvrval2  28153  cvrnbtwn2  28154  ishlat2  28232  3dim0  28335  islvol5  28457  pmapjat1  28731  pclcmpatN  28779  pclfinclN  28828  cdlemefrs29pre00  29273  cdlemefrs29bpre0  29274  cdlemefrs29cpre1  29276  cdleme32a  29319  cdlemftr3  29443  dvhopellsm  29996  dibelval3  30026  diblsmopel  30050  mapdvalc  30508  mapdval4N  30511  mapdordlem1a  30513
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