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  24346  nocvxminlem  24414  nofulllem1  24426  nofulllem5  24430  brtxp2  24491  brpprod3a  24496  elfuns  24524  brcart  24541  brsuccf  24550  ax5seg  24637  broutsideof3  24820  df3nandALT2  24907  andnand1  24908  itg2addnclem2  25003  itg2gt0cn  25005  iblabsnclem  25013  areacirc  25033  and4com  25042  isidlNEW  25548  svs2  25589  svs3  25590  isalg  25823  algi  25829  ishomc  25891  cinvlem3  25932  issubcata  25948  isibg2  26212  isside0  26266  bosser  26269  isibcg  26293  ivthALT  26360  islocfin  26398  neificl  26569  ablo4pnp  26672  isrngohom  26698  isidl  26741  ispridl  26761  pridlidl  26762  ismaxidl  26767  maxidlidl  26768  isfldidl2  26796  isdmn3  26801  fz1eqin  26950  issdrg  27607  sdrgacs  27611  isdomn3  27625  iotasbc2  27722  stoweidlem17  27868  stoweidlem34  27885  stoweidlem60  27911  ndmaovass  28173  ndmaovdistr  28174  3biant1d  28179  mpt2xopovel  28201  nbgrael  28274  nb3grapr2  28289  wlks  28327  iswlkon  28331  trls  28334  pths  28351  0pth  28355  1to3vfriswmgra  28430  eelT00  28784  eelTTT  28785  eelT11  28787  eelT12  28791  eelTT1  28793  eelT01  28794  eel0T1  28795  uun132  28873  uun132p1  28874  un2122  28878  uunTT1  28881  uunTT1p1  28882  uunTT1p2  28883  uunT11  28884  uunT11p1  28885  uunT11p2  28886  uunT12  28887  uunT12p1  28888  uunT12p2  28889  uunT12p3  28890  uunT12p4  28891  uunT12p5  28892  uun111  28893  uun2221  28901  uun2221p1  28902  uun2221p2  28903  bnj250  29041  bnj255  29045  bnj345  29054  bnj945  29120  bnj1209  29144  bnj1275  29161  bnj543  29240  bnj571  29253  bnj607  29263  bnj882  29273  bnj983  29298  bnj996  29302  bnj1006  29306  bnj1033  29314  bnj1097  29326  bnj1110  29327  bnj1145  29338  bnj1174  29348  bnj1189  29354  bnj1450  29395  bnj1514  29408  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