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

Theorem 3anass 940
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 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 anass 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
31, 2bitri 241 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3anrot  941  3anan12  949  3biant1d  1292  3exdistr  1929  r3al  2723  ceqsex2  2952  ceqsex3v  2954  ceqsex4v  2955  ceqsex6v  2956  ceqsex8v  2957  2reu5lem1  3099  2reu5lem2  3100  2reu5lem3  3101  trel3  4270  ordelord  4563  dflim2  4597  dflim3  4786  dflim4  4787  dff1o4  5641  ndmovass  6194  ndmovdistr  6195  mpt2xopovel  6430  dfsmo2  6568  oeeui  6804  ecopovtrn  6966  elixp2  7025  elixp  7028  mptelixpg  7058  zorn2lem7  8338  grothprim  8665  grothtsk  8666  divmuldiv  9670  sup3  9921  dfnn3  9970  prime  10306  eluz2  10450  raluz2  10482  elixx1  10881  elixx3g  10885  elioo2  10913  elioo5  10924  elicc4  10933  iccneg  10974  icoshft  10975  difreicc  10984  elfz1  11004  elfz  11005  elfz2  11006  elfz2nn0  11038  elfzm11  11071  elfzo2  11098  elfzo3  11110  lbfzo0  11125  fzind2  11153  rediv  11891  imdiv  11898  cosmul  12729  bitsval  12891  bitsmod  12903  bitscmp  12905  smueqlem  12957  elgz  13254  xpsfrnel  13743  xpsfrnel2  13745  ismre  13770  mreexexlem4d  13827  iscatd2  13861  isssc  13975  eldmcoa  14175  isdrs  14346  isipodrs  14542  ismhm  14695  mhmpropd  14699  issubm  14703  submacs  14720  issubg  14899  eqglact  14946  eqgid  14947  isslw  15197  efgsdm  15317  mulgmhm  15405  mulgghm  15406  dmdprd  15514  dprdw  15523  subgdmdprd  15547  dmdprdpr  15562  isrng  15623  rnglghm  15666  dfrhm2  15776  issubrg3  15851  islmod  15909  lsspropd  16048  islmhm  16058  islbs  16103  lbspropd  16126  isphl  16814  elocv  16850  isobs  16902  istps3OLD  16942  neindisj  17136  lmbrf  17278  hauscmplem  17423  llyi  17490  subislly  17497  uptx  17610  txcn  17611  qtopeu  17701  elmptrab  17812  isfbas  17814  trfil2  17872  flimcls  17970  cnextcn  18051  psmettri2  18293  xmetec  18417  metuel2  18562  ngppropd  18631  bl2ioo  18776  xrtgioo  18790  om1elbas  19010  elpi1  19023  isclm  19042  iscph  19086  tchcph  19147  lmmbr2  19165  lmmbrf  19168  iscau2  19183  caussi  19203  lmclim  19208  bcthlem1  19230  srabn  19267  ishl2  19277  evthicc2  19310  ovolfioo  19317  ovolficc  19318  iblcnlem1  19632  iblrelem  19635  iblre  19638  iblcn  19643  isuc1p  20016  ismon1p  20018  ellogrn  20410  logreclem  20613  atandm  20669  atandm2  20670  atandm3  20671  atans2  20724  dmarea  20749  dchrelbas4  20980  nbgrael  21391  nb3grapr2  21416  wlks  21479  wlkon  21483  trls  21489  is2wlk  21518  pths  21519  0pth  21523  isgrpo2  21738  issubgo  21844  ajval  22316  issh  22663  dmadjss  23343  adjeu  23345  adjval  23346  isst  23669  ishst  23670  xrdifh  24096  xdivpnfrp  24132  isofld  24188  eldifpr  24345  issibf  24601  probun  24630  erdszelem1  24830  cvmsval  24906  cvmliftiota  24941  snmlval  24971  zmodid2  25067  lediv2aALT  25070  tfrALTlem  25490  nocvxminlem  25558  nofulllem1  25570  nofulllem5  25574  brtxp2  25635  brpprod3a  25640  elfuns  25668  brcart  25685  brsuccf  25694  ax5seg  25781  broutsideof3  25964  df3nandALT2  26051  andnand1  26052  itg2gt0cn  26159  iblabsnclem  26167  areacirc  26187  ivthALT  26228  islocfin  26266  neificl  26349  ablo4pnp  26445  isrngohom  26471  isidl  26514  ispridl  26534  pridlidl  26535  ismaxidl  26540  maxidlidl  26541  isfldidl2  26569  isdmn3  26574  fz1eqin  26717  issdrg  27373  sdrgacs  27377  isdomn3  27391  iotasbc2  27488  stoweidlem17  27633  stoweidlem34  27650  stoweidlem60  27676  ndmaovass  27937  ndmaovdistr  27938  rexdifpr  27947  2elfz3nn0  27984  swrdccatin1  28016  swrdccatin12lem3  28024  usgra2pthspth  28035  usgra2adedgspthlem2  28044  usgra2adedgwlkon  28047  2pthwlkonot  28082  usg2spthonot  28085  1to3vfriswmgra  28111  eelT00  28517  eelTTT  28518  eelT11  28520  eelT12  28524  eelTT1  28526  eelT01  28527  eel0T1  28528  uun132  28606  uun132p1  28607  un2122  28611  uunTT1  28614  uunTT1p1  28615  uunTT1p2  28616  uunT11  28617  uunT11p1  28618  uunT11p2  28619  uunT12  28620  uunT12p1  28621  uunT12p2  28622  uunT12p3  28623  uunT12p4  28624  uunT12p5  28625  uun111  28626  uun2221  28634  uun2221p1  28635  uun2221p2  28636  bnj250  28771  bnj255  28775  bnj345  28784  bnj945  28850  bnj1209  28874  bnj1275  28891  bnj543  28970  bnj571  28983  bnj607  28993  bnj882  29003  bnj983  29028  bnj996  29032  bnj1006  29036  bnj1033  29044  bnj1097  29056  bnj1110  29057  bnj1145  29068  bnj1174  29078  bnj1189  29084  bnj1450  29125  bnj1514  29138  islshp  29462  isopos  29663  cvrfval  29751  cvrval  29752  isatl  29782  isat3  29790  islpln5  30017  4atlem11  30091  dalem20  30175  lhpexle3  30494  lhpex2leN  30495  isltrn2N  30602  diclspsn  31677  lcfls1lem  32017  lcfls1N  32018
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  df-3an 938
  Copyright terms: Public domain W3C validator