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

Theorem 3anass 941
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 939 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 anass 632 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
31, 2bitri 242 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3anrot  942  3anan12  950  3biant1d  1293  3exdistr  1934  r3al  2764  ceqsex2  2993  ceqsex3v  2995  ceqsex4v  2996  ceqsex6v  2997  ceqsex8v  2998  2reu5lem1  3140  2reu5lem2  3141  2reu5lem3  3142  trel3  4311  ordelord  4604  dflim2  4638  dflim3  4828  dflim4  4829  dff1o4  5683  ndmovass  6236  ndmovdistr  6237  mpt2xopovel  6472  dfsmo2  6610  oeeui  6846  ecopovtrn  7008  elixp2  7067  elixp  7070  mptelixpg  7100  zorn2lem7  8383  grothprim  8710  grothtsk  8711  divmuldiv  9715  sup3  9966  dfnn3  10015  prime  10351  eluz2  10495  raluz2  10527  elixx1  10926  elixx3g  10930  elioo2  10958  elioo5  10969  elicc4  10978  iccneg  11019  icoshft  11020  difreicc  11029  elfz1  11049  elfz  11050  elfz2  11051  elfz2nn0  11083  elfzm11  11117  elfzo2  11144  elfzo3  11156  lbfzo0  11171  fzind2  11199  rediv  11937  imdiv  11944  cosmul  12775  bitsval  12937  bitsmod  12949  bitscmp  12951  smueqlem  13003  elgz  13300  xpsfrnel  13789  xpsfrnel2  13791  ismre  13816  mreexexlem4d  13873  iscatd2  13907  isssc  14021  eldmcoa  14221  isdrs  14392  isipodrs  14588  ismhm  14741  mhmpropd  14745  issubm  14749  submacs  14766  issubg  14945  eqglact  14992  eqgid  14993  isslw  15243  efgsdm  15363  mulgmhm  15451  mulgghm  15452  dmdprd  15560  dprdw  15569  subgdmdprd  15593  dmdprdpr  15608  isrng  15669  rnglghm  15712  dfrhm2  15822  issubrg3  15897  islmod  15955  lsspropd  16094  islmhm  16104  islbs  16149  lbspropd  16172  isphl  16860  elocv  16896  isobs  16948  istps3OLD  16988  neindisj  17182  lmbrf  17325  hauscmplem  17470  llyi  17538  subislly  17545  uptx  17658  txcn  17659  qtopeu  17749  elmptrab  17860  isfbas  17862  trfil2  17920  flimcls  18018  cnextcn  18099  psmettri2  18341  xmetec  18465  metuel2  18610  ngppropd  18679  bl2ioo  18824  xrtgioo  18838  om1elbas  19058  elpi1  19071  isclm  19090  iscph  19134  tchcph  19195  lmmbr2  19213  lmmbrf  19216  iscau2  19231  caussi  19251  lmclim  19256  bcthlem1  19278  srabn  19315  ishl2  19325  evthicc2  19358  ovolfioo  19365  ovolficc  19366  iblcnlem1  19680  iblrelem  19683  iblre  19686  iblcn  19691  isuc1p  20064  ismon1p  20066  ellogrn  20458  logreclem  20661  atandm  20717  atandm2  20718  atandm3  20719  atans2  20772  dmarea  20797  dchrelbas4  21028  nbgrael  21439  nb3grapr2  21464  wlks  21527  wlkon  21531  trls  21537  is2wlk  21566  pths  21567  0pth  21571  isgrpo2  21786  issubgo  21892  ajval  22364  issh  22711  dmadjss  23391  adjeu  23393  adjval  23394  isst  23717  ishst  23718  xrdifh  24144  xdivpnfrp  24180  isofld  24236  eldifpr  24393  issibf  24649  probun  24678  erdszelem1  24878  cvmsval  24954  cvmliftiota  24989  snmlval  25019  zmodid2  25115  lediv2aALT  25118  elwlim  25575  nocvxminlem  25646  nofulllem1  25658  nofulllem5  25662  brtxp2  25727  brpprod3a  25732  brcart  25778  brsuccf  25787  ax5seg  25878  broutsideof3  26061  df3nandALT2  26148  andnand1  26149  itg2gt0cn  26261  iblabsnclem  26269  areacirc  26298  ivthALT  26339  islocfin  26377  neificl  26460  ablo4pnp  26556  isrngohom  26582  isidl  26625  ispridl  26645  pridlidl  26646  ismaxidl  26651  maxidlidl  26652  isfldidl2  26680  isdmn3  26685  fz1eqin  26828  issdrg  27483  sdrgacs  27487  isdomn3  27501  iotasbc2  27598  stoweidlem17  27743  stoweidlem34  27760  stoweidlem60  27786  ndmaovass  28047  ndmaovdistr  28048  rexdifpr  28060  uzletr  28104  2elfz3nn0  28113  swrdvalodm2  28189  swrdvalodm  28190  swrdccatin1  28206  swrdccat  28217  2cshw2lem1  28253  2wlkeq  28304  usgra2pthspth  28306  usgra2adedgspthlem2  28315  usgra2adedgwlkon  28318  2pthwlkonot  28353  usg2spthonot  28356  isrusgra  28371  1to3vfriswmgra  28398  eelT00  28809  eelTTT  28810  eelT11  28812  eelT12  28816  eelTT1  28818  eelT01  28819  eel0T1  28820  uun132  28898  uun132p1  28899  un2122  28903  uunTT1  28906  uunTT1p1  28907  uunTT1p2  28908  uunT11  28909  uunT11p1  28910  uunT11p2  28911  uunT12  28912  uunT12p1  28913  uunT12p2  28914  uunT12p3  28915  uunT12p4  28916  uunT12p5  28917  uun111  28918  uun2221  28926  uun2221p1  28927  uun2221p2  28928  bnj250  29066  bnj255  29070  bnj345  29079  bnj945  29145  bnj1209  29169  bnj1275  29186  bnj543  29265  bnj571  29278  bnj607  29288  bnj882  29298  bnj983  29323  bnj996  29327  bnj1006  29331  bnj1033  29339  bnj1097  29351  bnj1110  29352  bnj1145  29363  bnj1174  29373  bnj1189  29379  bnj1450  29420  bnj1514  29433  islshp  29778  isopos  29979  cvrfval  30067  cvrval  30068  isatl  30098  isat3  30106  islpln5  30333  4atlem11  30407  dalem20  30491  lhpexle3  30810  lhpex2leN  30811  isltrn2N  30918  diclspsn  31993  lcfls1lem  32333  lcfls1N  32334
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator