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  1883  2sb5  2084  2sb5rf  2089  sbel2x  2097  r2exf  2613  r19.41  2726  ceqsex3v  2860  ceqsrex2v  2937  rexrab  2963  rexrab2  2967  2reu5  3007  rexss  3274  inass  3413  indifdir  3459  difin2  3464  difrab  3476  reupick3  3487  inssdif0  3555  rexdifsn  3787  eqvinop  4288  copsexg  4289  wefrc  4424  uniuni  4564  reusv2lem4  4575  reusv2  4577  rabxp  4762  elvvv  4786  resopab2  5036  ssrnres  5153  elxp4  5197  elxp5  5198  cnvresima  5199  mptpreima  5203  coass  5228  imadif  5364  dff1o2  5515  eqfnfv3  5662  rexsupp  5688  isoini  5877  f1oiso  5890  oprabid  5924  dfoprab2  5937  mpt2eq123  5949  mpt2mptx  5980  resoprab2  5983  oprabex3  6004  ov3  6026  difxp  6195  frxp  6267  brtpos2  6282  oeeui  6642  oeeu  6643  omabs  6687  mapsnen  6981  xpsnen  6989  xpcomco  6995  xpassen  6999  wemapso2lem  7310  epfrs  7458  bnd2  7608  aceq1  7789  dfac5lem1  7795  dfac5lem2  7796  dfac5lem5  7799  kmlem3  7823  kmlem14  7834  pwfseqlem1  8325  ltexpi  8571  ltexprlem4  8708  axaddf  8812  axmulf  8813  rexuz  10316  rexuz2  10317  nnwos  10333  zmin  10359  rexrp  10420  elixx3g  10716  elfz2  10836  fzind2  10970  hashbclem  11437  resqrex  11783  rlim  12016  divalglem10  12648  divalgb  12650  gcdass  12771  isprm2  12813  infpn2  13007  ispos2  14131  issubg3  14686  resscntz  14856  subgdmdprd  15318  dprd2d2  15328  dfrhm2  15547  isassa  16105  aspval2  16135  istps2OLD  16715  istps3OLD  16716  ntreq0  16870  cmpcov2  17173  llyi  17256  nllyi  17257  subislly  17263  ptpjpre1  17322  tx1cn  17359  tx2cn  17360  txtube  17390  txkgen  17402  trfil2  17634  elflim2  17711  cnpflfi  17746  isfcls  17756  istlm  17919  blres  18029  metrest  18122  isnlm  18238  elcncf1di  18451  elpi1  18596  iscph  18659  itg1climres  19122  itgsubst  19449  ulmdvlem3  19832  cubic  20198  vmasum  20508  logfac2  20509  lgsquadlem1  20646  lgsquadlem2  20647  grpoidinvlem3  20926  h2hlm  21615  issh  21842  issh3  21854  ocsh  21917  cvbr2  22918  cvnbtwn2  22922  mdsl2i  22957  cvmdi  22959  mdsymlem2  23039  sumdmdii  23050  1stpreima  23245  2ndpreima  23246  cfilucfil3  23504  1stmbfm  23784  2ndmbfm  23785  dya2icoseg2  23802  dya2iocnei  23806  iscvm  24074  axacprim  24337  dfpo2  24497  dfdm5  24517  dfrn5  24518  preduz  24585  wfi  24592  frind  24628  sltval2  24695  nofulllem5  24745  dfon3  24817  elfuns  24839  brimg  24861  brsuccf  24865  dfrdg4  24874  tfrqfree  24875  axcontlem5  24982  ifscgr  25053  cgrxfr  25064  segcon2  25114  seglecgr12im  25119  segletr  25123  ellines  25161  itg2addnc  25319  areacirclem6  25347  cnvresimaOLD  25375  neifg  25469  isbnd2  25655  heibor1  25682  prtlem70  25863  prtlem100  25869  diophrex  26003  rmxdioph  26257  dford4  26270  islmodfg  26315  islssfg2  26317  isdomn3  26671  fgraphopab  26677  2sbc5g  26764  nb3grapr2  27400  trls  27448  3v3e3cycl2  27548  1to2vfriswmgra  27598  bnj250  28237  bnj251  28238  bnj256  28242  bnj168  28269  2sb5NEW7  28776  sbel2xNEW7  28781  2sb5rfOLD7  28913  lsateln0  29003  islshpat  29025  lcvbr2  29030  lcvnbtwn2  29035  isopos  29188  cvrval2  29282  cvrnbtwn2  29283  ishlat2  29361  3dim0  29464  islvol5  29586  pmapjat1  29860  pclcmpatN  29908  pclfinclN  29957  cdlemefrs29pre00  30402  cdlemefrs29bpre0  30403  cdlemefrs29cpre1  30405  cdleme32a  30448  cdlemftr3  30572  dvhopellsm  31125  dibelval3  31155  diblsmopel  31179  mapdvalc  31637  mapdval4N  31640  mapdordlem1a  31642
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