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  1854  2sb5  2054  2sb5rf  2059  sbel2x  2067  r2exf  2580  r19.41  2693  ceqsex3v  2827  ceqsrex2v  2904  rexrab  2930  rexrab2  2934  2reu5  2974  rexss  3241  inass  3380  indifdir  3426  difin2  3431  difrab  3443  reupick3  3454  inssdif0  3522  rexdifsn  3754  eqvinop  4250  copsexg  4251  wefrc  4386  uniuni  4526  reusv2lem4  4537  reusv2  4539  rabxp  4724  elvvv  4748  resopab2  4998  ssrnres  5115  elxp4  5158  elxp5  5159  cnvresima  5160  mptpreima  5164  coass  5189  imadif  5293  dff1o2  5443  eqfnfv3  5586  rexsupp  5612  isoini  5797  f1oiso  5810  oprabid  5844  dfoprab2  5857  mpt2eq123  5869  mpt2mptx  5900  resoprab2  5903  oprabex3  5924  ov3  5946  difxp  6115  frxp  6187  brtpos2  6202  oeeui  6596  oeeu  6597  omabs  6641  mapsnen  6934  xpsnen  6942  xpcomco  6948  xpassen  6952  wemapso2lem  7261  epfrs  7409  bnd2  7559  aceq1  7740  dfac5lem1  7746  dfac5lem2  7747  dfac5lem5  7750  kmlem3  7774  kmlem14  7785  pwfseqlem1  8276  ltexpi  8522  ltexprlem4  8659  axaddf  8763  axmulf  8764  rexuz  10265  rexuz2  10266  nnwos  10282  zmin  10308  rexrp  10369  elixx3g  10665  elfz2  10785  fzind2  10919  hashbclem  11386  resqrex  11732  rlim  11965  divalglem10  12597  divalgb  12599  gcdass  12720  isprm2  12762  infpn2  12956  ispos2  14078  issubg3  14633  resscntz  14803  subgdmdprd  15265  dprd2d2  15275  dfrhm2  15494  isassa  16052  aspval2  16082  istps2OLD  16655  istps3OLD  16656  ntreq0  16810  cmpcov2  17113  llyi  17196  nllyi  17197  subislly  17203  ptpjpre1  17262  tx1cn  17299  tx2cn  17300  txtube  17330  txkgen  17342  trfil2  17578  elflim2  17655  cnpflfi  17690  isfcls  17700  istlm  17863  blres  17973  metrest  18066  isnlm  18182  elcncf1di  18395  elpi1  18539  iscph  18602  itg1climres  19065  itgsubst  19392  ulmdvlem3  19775  cubic  20141  vmasum  20451  logfac2  20452  lgsquadlem1  20589  lgsquadlem2  20590  grpoidinvlem3  20867  h2hlm  21556  issh  21783  issh3  21795  ocsh  21858  cvbr2  22859  cvnbtwn2  22863  mdsl2i  22898  cvmdi  22900  mdsymlem2  22980  sumdmdii  22991  iscvm  23197  axacprim  23460  dfpo2  23518  dfdm5  23536  dfrn5  23537  preduz  23604  wfi  23611  frind  23647  sltval2  23713  dfon3  23843  brimg  23886  brsuccf  23890  dfrdg4  23898  tfrqfree  23899  axcontlem5  24006  ifscgr  24077  cgrxfr  24088  segcon2  24138  seglecgr12im  24143  segletr  24147  ellines  24185  areacirclem6  24340  eqvinopb  24375  copsexgb  24376  elo  24451  dfdir2  24702  cnvresimaOLD  25637  neifg  25731  isbnd2  25918  heibor1  25945  prtlem70  26126  prtlem100  26132  diophrex  26266  rmxdioph  26520  dford4  26533  islmodfg  26578  islssfg2  26580  isdomn3  26934  fgraphopab  26940  2sbc5g  27027  bnj250  28005  bnj251  28006  bnj256  28010  bnj168  28037  lsateln0  28464  islshpat  28486  lcvbr2  28491  lcvnbtwn2  28496  isopos  28649  cvrval2  28743  cvrnbtwn2  28744  ishlat2  28822  3dim0  28925  islvol5  29047  pmapjat1  29321  pclcmpatN  29369  pclfinclN  29418  cdlemefrs29pre00  29863  cdlemefrs29bpre0  29864  cdlemefrs29cpre1  29866  cdleme32a  29909  cdlemftr3  30033  dvhopellsm  30586  dibelval3  30616  diblsmopel  30640  mapdvalc  31098  mapdval4N  31101  mapdordlem1a  31103
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