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

Theorem anass 631
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 20 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ph  /\  ( ps  /\  ch ) ) )
21anassrs 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ph  /\  ( ps  /\  ch ) ) )
3 id 20 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ( ph  /\  ps )  /\  ch )
)
43anasss 629 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ( ph  /\  ps )  /\  ch )
)
52, 4impbii 181 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an12  773  an32  774  an13  775  an31  776  an4  798  3anass  940  4exdistrOLD  1924  2sb5  2145  2sb5rf  2151  sbel2x  2159  r2exf  2685  r19.41  2803  ceqsex3v  2937  ceqsrex2v  3014  rexrab  3041  rexrab2  3045  2reu5  3085  rexss  3353  inass  3494  indifdir  3540  difin2  3546  difrab  3558  reupick3  3569  inssdif0  3638  rexdifsn  3874  eqvinop  4382  copsexg  4383  wefrc  4517  uniuni  4656  reusv2lem4  4667  reusv2  4669  rabxp  4854  elvvv  4877  resopab2  5130  ssrnres  5249  elxp4  5297  elxp5  5298  cnvresima  5299  mptpreima  5303  coass  5328  imadif  5468  dff1o2  5619  eqfnfv3  5768  rexsupp  5794  isoini  5997  f1oiso  6010  oprabid  6044  dfoprab2  6060  mpt2eq123  6072  mpt2mptx  6103  resoprab2  6106  oprabex3  6127  ov3  6149  difxp  6319  frxp  6392  brtpos2  6421  oeeui  6781  oeeu  6782  omabs  6826  mapsnen  7120  xpsnen  7128  xpcomco  7134  xpassen  7138  wemapso2lem  7452  epfrs  7600  bnd2  7750  aceq1  7931  dfac5lem1  7937  dfac5lem2  7938  dfac5lem5  7941  kmlem3  7965  kmlem14  7976  pwfseqlem1  8466  ltexpi  8712  ltexprlem4  8849  axaddf  8953  axmulf  8954  rexuz  10459  rexuz2  10460  nnwos  10476  zmin  10502  rexrp  10563  elixx3g  10861  elfz2  10982  fzind2  11125  hashbclem  11628  resqrex  11983  rlim  12216  divalglem10  12849  divalgb  12851  gcdass  12972  isprm2  13014  infpn2  13208  ispos2  14332  issubg3  14887  resscntz  15057  subgdmdprd  15519  dprd2d2  15529  dfrhm2  15748  isassa  16302  aspval2  16332  istps2OLD  16909  istps3OLD  16910  ntreq0  17064  cmpcov2  17375  llyi  17458  nllyi  17459  subislly  17465  ptpjpre1  17524  tx1cn  17562  tx2cn  17563  txtube  17593  txkgen  17605  trfil2  17840  elflim2  17917  cnpflfi  17952  isfcls  17962  cnextcn  18019  istlm  18135  blres  18351  metrest  18444  isnlm  18582  elcncf1di  18796  elpi1  18941  iscph  19004  cfilucfil3  19142  itg1climres  19473  itgsubst  19800  ulmdvlem3  20185  cubic  20556  vmasum  20867  logfac2  20868  lgsquadlem1  21005  lgsquadlem2  21006  nb3grapr2  21329  trls  21400  3v3e3cycl2  21499  grpoidinvlem3  21642  h2hlm  22331  issh  22558  issh3  22570  ocsh  22633  cvbr2  23634  cvnbtwn2  23638  mdsl2i  23673  cvmdi  23675  mdsymlem2  23755  sumdmdii  23766  1stpreima  23936  2ndpreima  23937  1stmbfm  24404  2ndmbfm  24405  dya2iocnei  24426  iscvm  24725  axacprim  24935  dfpo2  25136  dfdm5  25156  dfrn5  25157  preduz  25224  wfi  25231  frind  25267  sltval2  25334  nofulllem5  25384  dfon3  25456  elfuns  25478  brimg  25500  brsuccf  25504  dfrdg4  25513  tfrqfree  25514  axcontlem5  25621  ifscgr  25692  cgrxfr  25703  segcon2  25753  seglecgr12im  25758  segletr  25762  ellines  25800  itg2addnc  25959  areacirclem6  25987  neifg  26091  isbnd2  26183  heibor1  26210  prtlem70  26389  prtlem100  26395  diophrex  26525  rmxdioph  26778  dford4  26791  islmodfg  26836  islssfg2  26838  isdomn3  27192  fgraphopab  27198  2sbc5g  27285  1to2vfriswmgra  27759  bnj250  28403  bnj251  28404  bnj256  28408  bnj168  28435  2sb5NEW7  28942  sbel2xNEW7  28947  2sb5rfOLD7  29078  lsateln0  29110  islshpat  29132  lcvbr2  29137  lcvnbtwn2  29142  isopos  29295  cvrval2  29389  cvrnbtwn2  29390  ishlat2  29468  3dim0  29571  islvol5  29693  pmapjat1  29967  pclcmpatN  30015  pclfinclN  30064  cdlemefrs29pre00  30509  cdlemefrs29bpre0  30510  cdlemefrs29cpre1  30512  cdleme32a  30555  cdlemftr3  30679  dvhopellsm  31232  dibelval3  31262  diblsmopel  31286  mapdvalc  31744  mapdval4N  31747  mapdordlem1a  31749
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 178  df-an 361
  Copyright terms: Public domain W3C validator