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

Theorem 3anass 938
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 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 anass 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
31, 2bitri 240 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anrot  939  3anan12  947  3exdistr  1863  r3al  2613  ceqsex2  2837  ceqsex3v  2839  ceqsex4v  2840  ceqsex6v  2841  ceqsex8v  2842  2reu5lem1  2983  2reu5lem2  2984  2reu5lem3  2985  trel3  4137  ordelord  4430  dflim2  4464  dflim3  4654  dflim4  4655  dff1o4  5496  ndmovass  6024  ndmovdistr  6025  dfsmo2  6380  oeeui  6616  ecopovtrn  6777  elixp2  6836  elixp  6839  mptelixpg  6869  zorn2lem7  8145  grothprim  8472  grothtsk  8473  divmuldiv  9476  sup3  9727  dfnn3  9776  prime  10108  eluz2  10252  raluz2  10284  elixx1  10681  elixx3g  10685  elioo2  10713  elioo5  10724  elicc4  10733  iccneg  10773  icoshft  10774  difreicc  10783  elfz1  10803  elfz  10804  elfz2  10805  elfz2nn0  10837  elfzm11  10869  elfzo2  10894  elfzo3  10906  lbfzo0  10919  fzind2  10939  rediv  11632  imdiv  11639  cosmul  12469  bitsval  12631  bitsmod  12643  bitscmp  12645  smueqlem  12697  elgz  12994  xpsfrnel  13481  xpsfrnel2  13483  ismre  13508  mreexexlem4d  13565  iscatd2  13599  isssc  13713  eldmcoa  13913  isdrs  14084  isipodrs  14280  ismhm  14433  mhmpropd  14437  issubm  14441  submacs  14458  issubg  14637  eqglact  14684  eqgid  14685  isslw  14935  efgsdm  15055  mulgmhm  15143  mulgghm  15144  dmdprd  15252  dprdw  15261  subgdmdprd  15285  dmdprdpr  15300  isrng  15361  rnglghm  15404  dfrhm2  15514  issubrg3  15589  islmod  15647  lsspropd  15790  islmhm  15800  islbs  15845  lbspropd  15868  isphl  16548  elocv  16584  isobs  16636  istps3OLD  16676  neindisj  16870  lmbrf  17006  hauscmplem  17149  llyi  17216  subislly  17223  uptx  17335  txcn  17336  qtopeu  17423  elmptrab  17538  isfbas  17540  trfil2  17598  flimcls  17696  xmetec  17996  ngppropd  18169  bl2ioo  18314  xrtgioo  18328  om1elbas  18546  elpi1  18559  isclm  18578  iscph  18622  tchcph  18683  lmmbr2  18701  lmmbrf  18704  iscau2  18719  caussi  18739  lmclim  18744  bcthlem1  18762  srabn  18793  ishl2  18803  evthicc2  18836  ovolfioo  18843  ovolficc  18844  iblcnlem1  19158  iblrelem  19161  iblre  19164  iblcn  19169  itgsubst  19412  isuc1p  19542  ismon1p  19544  ellogrn  19933  logreclem  20132  atandm  20188  atandm2  20189  atandm3  20190  atans2  20243  dmarea  20268  dchrelbas4  20498  isgrpo2  20880  issubgo  20986  ajval  21456  issh  21803  dmadjss  22483  adjeu  22485  adjval  22486  isst  22809  ishst  22810  xdivpnfrp  23133  xrdifh  23288  eldifpr  23409  isibfm  23608  probun  23637  erdszelem1  23737  cvmsval  23812  cvmliftiota  23847  snmlval  23929  zmodid2  24025  lediv2aALT  24028  tfrALTlem  24347  nocvxminlem  24415  nofulllem1  24427  nofulllem5  24431  brtxp2  24492  brpprod3a  24497  elfuns  24525  brcart  24542  brsuccf  24551  ax5seg  24638  broutsideof3  24821  df3nandALT2  24908  andnand1  24909  itg2addnclem2  25004  itg2gt0cn  25006  iblabsnclem  25014  areacirc  25034  and4com  25043  isidlNEW  25549  svs2  25590  svs3  25591  isalg  25824  algi  25830  ishomc  25892  cinvlem3  25933  issubcata  25949  isibg2  26213  isside0  26267  bosser  26270  isibcg  26294  ivthALT  26361  islocfin  26399  neificl  26570  ablo4pnp  26673  isrngohom  26699  isidl  26742  ispridl  26762  pridlidl  26763  ismaxidl  26768  maxidlidl  26769  isfldidl2  26797  isdmn3  26802  fz1eqin  26951  issdrg  27608  sdrgacs  27612  isdomn3  27626  iotasbc2  27723  stoweidlem17  27869  stoweidlem34  27886  stoweidlem60  27912  ndmaovass  28174  ndmaovdistr  28175  3biant1d  28180  mpt2xopovel  28202  nbgrael  28275  nb3grapr2  28290  wlks  28328  iswlkon  28332  trls  28335  pths  28352  0pth  28356  1to3vfriswmgra  28431  eelT00  28785  eelTTT  28786  eelT11  28788  eelT12  28792  eelTT1  28794  eelT01  28795  eel0T1  28796  uun132  28874  uun132p1  28875  un2122  28879  uunTT1  28882  uunTT1p1  28883  uunTT1p2  28884  uunT11  28885  uunT11p1  28886  uunT11p2  28887  uunT12  28888  uunT12p1  28889  uunT12p2  28890  uunT12p3  28891  uunT12p4  28892  uunT12p5  28893  uun111  28894  uun2221  28902  uun2221p1  28903  uun2221p2  28904  bnj250  29042  bnj255  29046  bnj345  29055  bnj945  29121  bnj1209  29145  bnj1275  29162  bnj543  29241  bnj571  29254  bnj607  29264  bnj882  29274  bnj983  29299  bnj996  29303  bnj1006  29307  bnj1033  29315  bnj1097  29327  bnj1110  29328  bnj1145  29339  bnj1174  29349  bnj1189  29355  bnj1450  29396  bnj1514  29409  islshp  29791  isopos  29992  cvrfval  30080  cvrval  30081  isatl  30111  isat3  30119  islpln5  30346  4atlem11  30420  dalem20  30504  lhpexle3  30823  lhpex2leN  30824  isltrn2N  30931  diclspsn  32006  lcfls1lem  32346  lcfls1N  32347
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  df-3an 936
  Copyright terms: Public domain W3C validator