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

Theorem 3anass 941
Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anass  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )

Proof of Theorem 3anass
StepHypRef Expression
1 df-3an 939 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 anass 632 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
31, 2bitri 242 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3anrot  942  3anan12  950  3biant1d  1293  3exdistr  1934  r3al  2765  ceqsex2  2994  ceqsex3v  2996  ceqsex4v  2997  ceqsex6v  2998  ceqsex8v  2999  2reu5lem1  3141  2reu5lem2  3142  2reu5lem3  3143  trel3  4313  ordelord  4606  dflim2  4640  dflim3  4830  dflim4  4831  dff1o4  5685  ndmovass  6238  ndmovdistr  6239  mpt2xopovel  6474  dfsmo2  6612  oeeui  6848  ecopovtrn  7010  elixp2  7069  elixp  7072  mptelixpg  7102  zorn2lem7  8387  grothprim  8714  grothtsk  8715  divmuldiv  9719  sup3  9970  dfnn3  10019  prime  10355  eluz2  10499  raluz2  10531  elixx1  10930  elixx3g  10934  elioo2  10962  elioo5  10973  elicc4  10982  iccneg  11023  icoshft  11024  difreicc  11033  elfz1  11053  elfz  11054  elfz2  11055  elfz2nn0  11087  elfzm11  11121  elfzo2  11148  elfzo3  11160  lbfzo0  11175  fzind2  11203  rediv  11941  imdiv  11948  cosmul  12779  bitsval  12941  bitsmod  12953  bitscmp  12955  smueqlem  13007  elgz  13304  xpsfrnel  13793  xpsfrnel2  13795  ismre  13820  mreexexlem4d  13877  iscatd2  13911  isssc  14025  eldmcoa  14225  isdrs  14396  isipodrs  14592  ismhm  14745  mhmpropd  14749  issubm  14753  submacs  14770  issubg  14949  eqglact  14996  eqgid  14997  isslw  15247  efgsdm  15367  mulgmhm  15455  mulgghm  15456  dmdprd  15564  dprdw  15573  subgdmdprd  15597  dmdprdpr  15612  isrng  15673  rnglghm  15716  dfrhm2  15826  issubrg3  15901  islmod  15959  lsspropd  16098  islmhm  16108  islbs  16153  lbspropd  16176  isphl  16864  elocv  16900  isobs  16952  istps3OLD  16992  neindisj  17186  lmbrf  17329  hauscmplem  17474  llyi  17542  subislly  17549  uptx  17662  txcn  17663  qtopeu  17753  elmptrab  17864  isfbas  17866  trfil2  17924  flimcls  18022  cnextcn  18103  psmettri2  18345  xmetec  18469  metuel2  18614  ngppropd  18683  bl2ioo  18828  xrtgioo  18842  om1elbas  19062  elpi1  19075  isclm  19094  iscph  19138  tchcph  19199  lmmbr2  19217  lmmbrf  19220  iscau2  19235  caussi  19255  lmclim  19260  bcthlem1  19282  srabn  19319  ishl2  19329  evthicc2  19362  ovolfioo  19369  ovolficc  19370  iblcnlem1  19682  iblrelem  19685  iblre  19688  iblcn  19693  isuc1p  20068  ismon1p  20070  ellogrn  20462  logreclem  20665  atandm  20721  atandm2  20722  atandm3  20723  atans2  20776  dmarea  20801  dchrelbas4  21032  nbgrael  21443  nb3grapr2  21468  wlks  21531  wlkon  21535  trls  21541  is2wlk  21570  pths  21571  0pth  21575  isgrpo2  21790  issubgo  21896  ajval  22368  issh  22715  dmadjss  23395  adjeu  23397  adjval  23398  isst  23721  ishst  23722  xrdifh  24148  xdivpnfrp  24184  isofld  24240  eldifpr  24397  issibf  24653  probun  24682  erdszelem1  24882  cvmsval  24958  cvmliftiota  24993  snmlval  25023  zmodid2  25119  lediv2aALT  25122  elwlim  25579  nocvxminlem  25650  nofulllem1  25662  nofulllem5  25666  brtxp2  25731  brpprod3a  25736  brcart  25782  brsuccf  25791  ax5seg  25882  broutsideof3  26065  df3nandALT2  26152  andnand1  26153  itg2gt0cn  26274  iblabsnclem  26282  areacirc  26311  ivthALT  26352  islocfin  26390  neificl  26473  ablo4pnp  26569  isrngohom  26595  isidl  26638  ispridl  26658  pridlidl  26659  ismaxidl  26664  maxidlidl  26665  isfldidl2  26693  isdmn3  26698  fz1eqin  26841  issdrg  27496  sdrgacs  27500  isdomn3  27514  iotasbc2  27611  stoweidlem17  27756  stoweidlem34  27773  stoweidlem60  27799  ndmaovass  28060  ndmaovdistr  28061  rexdifpr  28073  uzletr  28126  2elfz3nn0  28135  swrdvalodm2  28222  swrdvalodm  28223  swrdccatin1  28239  swrdccat  28250  2cshw2lem1  28286  2wlkeq  28341  usgra2pthspth  28343  usgra2adedgspthlem2  28352  usgra2adedgwlkon  28355  iswwlk  28365  wwlknimp  28369  2pthwlkonot  28417  usg2spthonot  28420  isrusgra  28442  1to3vfriswmgra  28471  eelT00  28882  eelTTT  28883  eelT11  28885  eelT12  28889  eelTT1  28891  eelT01  28892  eel0T1  28893  uun132  28971  uun132p1  28972  un2122  28976  uunTT1  28979  uunTT1p1  28980  uunTT1p2  28981  uunT11  28982  uunT11p1  28983  uunT11p2  28984  uunT12  28985  uunT12p1  28986  uunT12p2  28987  uunT12p3  28988  uunT12p4  28989  uunT12p5  28990  uun111  28991  uun2221  28999  uun2221p1  29000  uun2221p2  29001  bnj250  29139  bnj255  29143  bnj345  29152  bnj945  29218  bnj1209  29242  bnj1275  29259  bnj543  29338  bnj571  29351  bnj607  29361  bnj882  29371  bnj983  29396  bnj996  29400  bnj1006  29404  bnj1033  29412  bnj1097  29424  bnj1110  29425  bnj1145  29436  bnj1174  29446  bnj1189  29452  bnj1450  29493  bnj1514  29506  islshp  29851  isopos  30052  cvrfval  30140  cvrval  30141  isatl  30171  isat3  30179  islpln5  30406  4atlem11  30480  dalem20  30564  lhpexle3  30883  lhpex2leN  30884  isltrn2N  30991  diclspsn  32066  lcfls1lem  32406  lcfls1N  32407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator