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  1922  r3al  2699  ceqsex2  2928  ceqsex3v  2930  ceqsex4v  2931  ceqsex6v  2932  ceqsex8v  2933  2reu5lem1  3075  2reu5lem2  3076  2reu5lem3  3077  trel3  4244  ordelord  4537  dflim2  4571  dflim3  4760  dflim4  4761  dff1o4  5615  ndmovass  6167  ndmovdistr  6168  mpt2xopovel  6400  dfsmo2  6538  oeeui  6774  ecopovtrn  6936  elixp2  6995  elixp  6998  mptelixpg  7028  zorn2lem7  8308  grothprim  8635  grothtsk  8636  divmuldiv  9639  sup3  9890  dfnn3  9939  prime  10275  eluz2  10419  raluz2  10451  elixx1  10850  elixx3g  10854  elioo2  10882  elioo5  10893  elicc4  10902  iccneg  10943  icoshft  10944  difreicc  10953  elfz1  10973  elfz  10974  elfz2  10975  elfz2nn0  11007  elfzm11  11039  elfzo2  11066  elfzo3  11078  lbfzo0  11093  fzind2  11118  rediv  11856  imdiv  11863  cosmul  12694  bitsval  12856  bitsmod  12868  bitscmp  12870  smueqlem  12922  elgz  13219  xpsfrnel  13708  xpsfrnel2  13710  ismre  13735  mreexexlem4d  13792  iscatd2  13826  isssc  13940  eldmcoa  14140  isdrs  14311  isipodrs  14507  ismhm  14660  mhmpropd  14664  issubm  14668  submacs  14685  issubg  14864  eqglact  14911  eqgid  14912  isslw  15162  efgsdm  15282  mulgmhm  15370  mulgghm  15371  dmdprd  15479  dprdw  15488  subgdmdprd  15512  dmdprdpr  15527  isrng  15588  rnglghm  15631  dfrhm2  15741  issubrg3  15816  islmod  15874  lsspropd  16013  islmhm  16023  islbs  16068  lbspropd  16091  isphl  16775  elocv  16811  isobs  16863  istps3OLD  16903  neindisj  17097  lmbrf  17239  hauscmplem  17384  llyi  17451  subislly  17458  uptx  17571  txcn  17572  qtopeu  17662  elmptrab  17773  isfbas  17775  trfil2  17833  flimcls  17931  cnextcn  18012  xmetec  18347  metuel2  18478  ngppropd  18542  bl2ioo  18687  xrtgioo  18701  om1elbas  18921  elpi1  18934  isclm  18953  iscph  18997  tchcph  19058  lmmbr2  19076  lmmbrf  19079  iscau2  19094  caussi  19114  lmclim  19119  bcthlem1  19139  srabn  19174  ishl2  19184  evthicc2  19217  ovolfioo  19224  ovolficc  19225  iblcnlem1  19539  iblrelem  19542  iblre  19545  iblcn  19550  isuc1p  19923  ismon1p  19925  ellogrn  20317  logreclem  20520  atandm  20576  atandm2  20577  atandm3  20578  atans2  20631  dmarea  20656  dchrelbas4  20887  nbgrael  21297  nb3grapr2  21322  wlks  21383  wlkon  21387  trls  21393  pths  21413  0pth  21417  isgrpo2  21626  issubgo  21732  ajval  22204  issh  22551  dmadjss  23231  adjeu  23233  adjval  23234  isst  23557  ishst  23558  xrdifh  23972  xdivpnfrp  24011  isofld  24054  eldifpr  24181  probun  24449  erdszelem1  24649  cvmsval  24725  cvmliftiota  24760  snmlval  24790  zmodid2  24886  lediv2aALT  24889  tfrALTlem  25293  nocvxminlem  25361  nofulllem1  25373  nofulllem5  25377  brtxp2  25438  brpprod3a  25443  elfuns  25471  brcart  25488  brsuccf  25497  ax5seg  25584  broutsideof3  25767  df3nandALT2  25854  andnand1  25855  itg2gt0cn  25953  iblabsnclem  25961  areacirc  25981  ivthALT  26022  islocfin  26060  neificl  26143  ablo4pnp  26239  isrngohom  26265  isidl  26308  ispridl  26328  pridlidl  26329  ismaxidl  26334  maxidlidl  26335  isfldidl2  26363  isdmn3  26368  fz1eqin  26511  issdrg  27167  sdrgacs  27171  isdomn3  27185  iotasbc2  27282  stoweidlem17  27427  stoweidlem34  27444  stoweidlem60  27470  ndmaovass  27732  ndmaovdistr  27733  1to3vfriswmgra  27753  eelT00  28142  eelTTT  28143  eelT11  28145  eelT12  28149  eelTT1  28151  eelT01  28152  eel0T1  28153  uun132  28231  uun132p1  28232  un2122  28236  uunTT1  28239  uunTT1p1  28240  uunTT1p2  28241  uunT11  28242  uunT11p1  28243  uunT11p2  28244  uunT12  28245  uunT12p1  28246  uunT12p2  28247  uunT12p3  28248  uunT12p4  28249  uunT12p5  28250  uun111  28251  uun2221  28259  uun2221p1  28260  uun2221p2  28261  bnj250  28396  bnj255  28400  bnj345  28409  bnj945  28475  bnj1209  28499  bnj1275  28516  bnj543  28595  bnj571  28608  bnj607  28618  bnj882  28628  bnj983  28653  bnj996  28657  bnj1006  28661  bnj1033  28669  bnj1097  28681  bnj1110  28682  bnj1145  28693  bnj1174  28703  bnj1189  28709  bnj1450  28750  bnj1514  28763  islshp  29145  isopos  29346  cvrfval  29434  cvrval  29435  isatl  29465  isat3  29473  islpln5  29700  4atlem11  29774  dalem20  29858  lhpexle3  30177  lhpex2leN  30178  isltrn2N  30285  diclspsn  31360  lcfls1lem  31700  lcfls1N  31701
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