MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anass Structured version   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  1935  2sb5  2187  2sb5rf  2193  sbel2x  2201  r2exf  2733  r19.41  2852  ceqsex3v  2986  ceqsrex2v  3063  rexrab  3090  rexrab2  3094  2reu5  3134  rexss  3402  inass  3543  indifdir  3589  difin2  3595  difrab  3607  reupick3  3618  inssdif0  3687  rexdifsn  3923  eqvinop  4433  copsexg  4434  wefrc  4568  uniuni  4708  reusv2lem4  4719  reusv2  4721  rabxp  4906  elvvv  4929  resopab2  5182  ssrnres  5301  elxp4  5349  elxp5  5350  cnvresima  5351  mptpreima  5355  coass  5380  imadif  5520  dff1o2  5671  eqfnfv3  5821  rexsupp  5847  isoini  6050  f1oiso  6063  oprabid  6097  dfoprab2  6113  mpt2eq123  6125  mpt2mptx  6156  resoprab2  6159  oprabex3  6180  ov3  6202  difxp  6372  frxp  6448  brtpos2  6477  oeeui  6837  oeeu  6838  omabs  6882  mapsnen  7176  xpsnen  7184  xpcomco  7190  xpassen  7194  wemapso2lem  7511  epfrs  7659  bnd2  7809  aceq1  7990  dfac5lem1  7996  dfac5lem2  7997  dfac5lem5  8000  kmlem3  8024  kmlem14  8035  pwfseqlem1  8525  ltexpi  8771  ltexprlem4  8908  axaddf  9012  axmulf  9013  rexuz  10519  rexuz2  10520  nnwos  10536  zmin  10562  rexrp  10623  elixx3g  10921  elfz2  11042  fzind2  11190  hashbclem  11693  resqrex  12048  rlim  12281  divalglem10  12914  divalgb  12916  gcdass  13037  isprm2  13079  infpn2  13273  ispos2  14397  issubg3  14952  resscntz  15122  subgdmdprd  15584  dprd2d2  15594  dfrhm2  15813  isassa  16367  aspval2  16397  istps2OLD  16978  istps3OLD  16979  ntreq0  17133  cmpcov2  17445  llyi  17529  nllyi  17530  subislly  17536  ptpjpre1  17595  tx1cn  17633  tx2cn  17634  txtube  17664  txkgen  17676  trfil2  17911  elflim2  17988  cnpflfi  18023  isfcls  18033  cnextcn  18090  istlm  18206  blres  18453  metrest  18546  isnlm  18703  elcncf1di  18917  elpi1  19062  iscph  19125  cfilucfil3OLD  19263  cfilucfil3  19264  itg1climres  19598  itgsubst  19925  ulmdvlem3  20310  cubic  20681  vmasum  20992  logfac2  20993  lgsquadlem1  21130  lgsquadlem2  21131  nb3grapr2  21455  trls  21528  3v3e3cycl2  21643  grpoidinvlem3  21786  h2hlm  22475  issh  22702  issh3  22714  ocsh  22777  cvbr2  23778  cvnbtwn2  23782  mdsl2i  23817  cvmdi  23819  mdsymlem2  23899  sumdmdii  23910  1stpreima  24087  2ndpreima  24088  1stmbfm  24602  2ndmbfm  24603  dya2iocnei  24624  iscvm  24938  axacprim  25148  dfpo2  25370  dfdm5  25392  dfrn5  25393  elima4  25396  preduz  25467  wfi  25474  frind  25510  sltval2  25603  nofulllem5  25653  dfon3  25729  brimg  25774  brsuccf  25778  dfrdg4  25787  tfrqfree  25788  axcontlem5  25899  ifscgr  25970  cgrxfr  25981  segcon2  26031  seglecgr12im  26036  segletr  26040  ellines  26078  itg2addnc  26249  ftc1anclem5  26274  ftc1anc  26278  areacirclem6  26287  neifg  26391  isbnd2  26483  heibor1  26510  prtlem70  26689  prtlem100  26695  diophrex  26825  rmxdioph  27078  dford4  27091  islmodfg  27135  islssfg2  27137  isdomn3  27491  fgraphopab  27497  2sbc5g  27584  rexdifpr  28049  usgra2pth0  28265  usg2spthonot0  28309  usg2spthonot1  28310  1to2vfriswmgra  28333  usgreg2spot  28393  bnj250  29002  bnj251  29003  bnj256  29007  bnj168  29034  2sb5NEW7  29546  sbel2xNEW7  29551  2sb5rfOLD7  29698  lsateln0  29730  islshpat  29752  lcvbr2  29757  lcvnbtwn2  29762  isopos  29915  cvrval2  30009  cvrnbtwn2  30010  ishlat2  30088  3dim0  30191  islvol5  30313  pmapjat1  30587  pclcmpatN  30635  pclfinclN  30684  cdlemefrs29pre00  31129  cdlemefrs29bpre0  31130  cdlemefrs29cpre1  31132  cdleme32a  31175  cdlemftr3  31299  dvhopellsm  31852  dibelval3  31882  diblsmopel  31906  mapdvalc  32364  mapdval4N  32367  mapdordlem1a  32369
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