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  1851  r3al  2600  ceqsex2  2824  ceqsex3v  2826  ceqsex4v  2827  ceqsex6v  2828  ceqsex8v  2829  2reu5lem1  2970  2reu5lem2  2971  2reu5lem3  2972  trel3  4121  ordelord  4414  dflim2  4448  dflim3  4638  dflim4  4639  dff1o4  5480  ndmovass  6008  ndmovdistr  6009  dfsmo2  6364  oeeui  6600  ecopovtrn  6761  elixp2  6820  elixp  6823  mptelixpg  6853  zorn2lem7  8129  grothprim  8456  grothtsk  8457  divmuldiv  9460  sup3  9711  dfnn3  9760  prime  10092  eluz2  10236  raluz2  10268  elixx1  10665  elixx3g  10669  elioo2  10697  elioo5  10708  elicc4  10717  iccneg  10757  icoshft  10758  difreicc  10767  elfz1  10787  elfz  10788  elfz2  10789  elfz2nn0  10821  elfzm11  10853  elfzo2  10878  elfzo3  10890  lbfzo0  10903  fzind2  10923  rediv  11616  imdiv  11623  cosmul  12453  bitsval  12615  bitsmod  12627  bitscmp  12629  smueqlem  12681  elgz  12978  xpsfrnel  13465  xpsfrnel2  13467  ismre  13492  mreexexlem4d  13549  iscatd2  13583  isssc  13697  eldmcoa  13897  isdrs  14068  isipodrs  14264  ismhm  14417  mhmpropd  14421  issubm  14425  submacs  14442  issubg  14621  eqglact  14668  eqgid  14669  isslw  14919  efgsdm  15039  mulgmhm  15127  mulgghm  15128  dmdprd  15236  dprdw  15245  subgdmdprd  15269  dmdprdpr  15284  isrng  15345  rnglghm  15388  dfrhm2  15498  issubrg3  15573  islmod  15631  lsspropd  15774  islmhm  15784  islbs  15829  lbspropd  15852  isphl  16532  elocv  16568  isobs  16620  istps3OLD  16660  neindisj  16854  lmbrf  16990  hauscmplem  17133  llyi  17200  subislly  17207  uptx  17319  txcn  17320  qtopeu  17407  elmptrab  17522  isfbas  17524  trfil2  17582  flimcls  17680  xmetec  17980  ngppropd  18153  bl2ioo  18298  xrtgioo  18312  om1elbas  18530  elpi1  18543  isclm  18562  iscph  18606  tchcph  18667  lmmbr2  18685  lmmbrf  18688  iscau2  18703  caussi  18723  lmclim  18728  bcthlem1  18746  srabn  18777  ishl2  18787  evthicc2  18820  ovolfioo  18827  ovolficc  18828  iblcnlem1  19142  iblrelem  19145  iblre  19148  iblcn  19153  itgsubst  19396  isuc1p  19526  ismon1p  19528  ellogrn  19917  logreclem  20116  atandm  20172  atandm2  20173  atandm3  20174  atans2  20227  dmarea  20252  dchrelbas4  20482  isgrpo2  20864  issubgo  20970  ajval  21440  issh  21787  dmadjss  22467  adjeu  22469  adjval  22470  isst  22793  ishst  22794  xdivpnfrp  23117  xrdifh  23273  eldifpr  23394  isibfm  23593  probun  23622  erdszelem1  23722  cvmsval  23797  cvmliftiota  23832  snmlval  23914  zmodid2  24010  lediv2aALT  24013  tfrALTlem  24276  nocvxminlem  24344  nofulllem1  24356  nofulllem5  24360  brtxp2  24421  brpprod3a  24426  elfuns  24454  brcart  24471  brsuccf  24480  ax5seg  24566  broutsideof3  24749  df3nandALT2  24836  andnand1  24837  areacirc  24931  and4com  24940  isidlNEW  25446  svs2  25487  svs3  25488  isalg  25721  algi  25727  ishomc  25789  cinvlem3  25830  issubcata  25846  isibg2  26110  isside0  26164  bosser  26167  isibcg  26191  ivthALT  26258  islocfin  26296  neificl  26467  ablo4pnp  26570  isrngohom  26596  isidl  26639  ispridl  26659  pridlidl  26660  ismaxidl  26665  maxidlidl  26666  isfldidl2  26694  isdmn3  26699  fz1eqin  26848  issdrg  27505  sdrgacs  27509  isdomn3  27523  iotasbc2  27620  stoweidlem17  27766  stoweidlem34  27783  stoweidlem60  27809  ndmaovass  28066  ndmaovdistr  28067  mpt2xopovel  28086  nbgrael  28141  1to3vfriswmgra  28185  eelT00  28480  eelTTT  28481  eelT11  28483  eelT12  28486  eelTT1  28488  eelT01  28489  eel0T1  28490  uun132  28560  uun132p1  28561  un2122  28565  uunTT1  28568  uunTT1p1  28569  uunTT1p2  28570  uunT11  28571  uunT11p1  28572  uunT11p2  28573  uunT12  28574  uunT12p1  28575  uunT12p2  28576  uunT12p3  28577  uunT12p4  28578  uunT12p5  28579  uun111  28580  uun2221  28588  uun2221p1  28589  uun2221p2  28590  bnj250  28726  bnj255  28730  bnj345  28739  bnj945  28805  bnj1209  28829  bnj1275  28846  bnj543  28925  bnj571  28938  bnj607  28948  bnj882  28958  bnj983  28983  bnj996  28987  bnj1006  28991  bnj1033  28999  bnj1097  29011  bnj1110  29012  bnj1145  29023  bnj1174  29033  bnj1189  29039  bnj1450  29080  bnj1514  29093  islshp  29169  isopos  29370  cvrfval  29458  cvrval  29459  isatl  29489  isat3  29497  islpln5  29724  4atlem11  29798  dalem20  29882  lhpexle3  30201  lhpex2leN  30202  isltrn2N  30309  diclspsn  31384  lcfls1lem  31724  lcfls1N  31725
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