Theorem 3anass 978

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

Step	Hyp	Ref	Expression
1		df-3an 976	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 649	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 249	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 184   /\ wa 369   /\ w3a 974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976

This theorem is referenced by:  3anrot  979  3anan12  987  anandi3  988  3biant1d  1338  an33rean  1343  3exdistr  1766  r3alOLD  2881  ceqsex2  3133  ceqsex3v  3135  ceqsex4v  3136  ceqsex6v  3137  ceqsex8v  3138  2reu5lem1  3291  2reu5lem2  3292  2reu5lem3  3293  eldifpr  4031  trel3  4538  ordelord  4890  dflim2  4924  dff1o4  5814  ndmovass  6448  ndmovdistr  6449  dflim3  6667  dflim4  6668  mpt2xopovel  6950  dfsmo2  7020  oeeui  7253  ecopovtrn  7416  elixp2  7475  elixp  7478  mptelixpg  7508  zorn2lem7  8885  grothprim  9215  grothtsk  9216  divmuldiv  10251  sup3  10507  dfnn3  10557  prime  10950  eluz2  11098  raluz2  11141  elixx1  11549  elixx3g  11553  elioo2  11581  elioo5  11593  elicc4  11602  iccneg  11652  icoshft  11653  difreicc  11663  elfz1  11688  elfz  11689  elfz2  11690  elfzm11  11760  elfz2nn0  11780  elfzo2  11814  elfzo3  11826  lbfzo0  11844  fzind2  11906  zmodid2  12006  ccatw2s1p1  12622  ccatw2s1p2  12623  swrdvalodm2  12646  swrdvalodm  12647  wrdeqswrdlsw  12656  swrdccatin1  12690  swrdccat  12700  repswswrd  12738  swrdco  12785  2swrd2eqwrdeq  12873  ccat2s1fvwALT  12875  rediv  12946  imdiv  12953  cosmul  13890  bitsval  14056  bitsmod  14068  bitscmp  14070  smueqlem  14122  elgz  14431  xpsfrnel  14942  xpsfrnel2  14944  ismre  14969  mreexexlem4d  15026  iscatd2  15060  isssc  15171  eldmcoa  15371  isdrs  15542  isipodrs  15770  ismhm  15947  mhmpropd  15951  issubm  15957  submacs  15975  issubg  16180  eqglact  16231  eqgid  16232  pgrpsubgsymgbi  16411  isslw  16607  efgsdm  16727  mulgmhm  16815  mulgghm  16816  dmdprd  17008  dprdw  17022  dprdwOLD  17029  subgdmdprd  17060  dmdprdpr  17077  issrg  17138  srglmhm  17165  srgrmhm  17166  isring  17181  ringlghm  17229  dfrhm2  17345  issubrg3  17436  islmod  17495  lsspropd  17642  islmhm  17652  islbs  17701  lbspropd  17724  isphl  18641  elocv  18677  isobs  18729  mat1dimscm  18955  scmatghm  19013  scmatmhm  19014  ma1repvcl  19050  smadiadetr  19155  mat2pmatghm  19209  mat2pmatmul  19210  decpmatmulsumfsupp  19252  pm2mpghm  19295  pm2mpmhmlem1  19297  istps3OLD  19401  neindisj  19596  lmbrf  19739  hauscmplem  19884  llyi  19953  subislly  19960  islocfin  19996  uptx  20104  txcn  20105  qtopeu  20195  elmptrab  20306  isfbas  20308  trfil2  20366  flimcls  20464  cnextcn  20545  xmetec  20915  ngppropd  21129  bl2ioo  21275  xrtgioo  21289  om1elbas  21510  elpi1  21523  isclm  21542  iscph  21595  tchcph  21658  lmmbr2  21676  lmmbrf  21679  iscau2  21694  caussi  21714  lmclim  21719  bcthlem1  21741  srabn  21778  ishl2  21788  evthicc2  21850  ovolfioo  21857  ovolficc  21858  iblcnlem1  22172  iblrelem  22175  iblre  22178  iblcn  22183  isuc1p  22519  ismon1p  22521  ellogrn  22925  logreclem  23128  atandm  23185  atandm2  23186  atandm3  23187  atans2  23240  dmarea  23265  dchrelbas4  23496  ax5seg  24219  eengtrkg  24266  nbgrael  24404  nb3grapr2  24432  wlks  24497  wlkon  24511  trls  24516  is2wlk  24545  pths  24546  0pth  24550  usgra2adedgspthlem2  24590  usgra2adedgwlkon  24593  iswwlk  24661  wwlknimp  24665  2wlkeq  24685  wwlkextwrd  24706  isclwwlk  24746  clwwlknprop  24750  clwwlkn2  24753  clwlkisclwwlklem0  24766  clwlkfclwwlk  24822  2pthwlkonot  24863  usg2spthonot  24866  isrusgra  24905  isrusgusrg  24910  isrusgrac  24913  rusgranumwlkl1  24925  rusgranumwlklem0  24926  1to3vfriswmgra  24985  numclwwlkovgel  25066  numclwwlk2lem1  25080  isgrpo2  25177  issubgo  25283  ajval  25755  issh  26103  dmadjss  26784  adjeu  26786  adjval  26787  isst  27110  ishst  27111  xrdifh  27569  nndiffz1  27574  xdivpnfrp  27607  isomnd  27669  isslmd  27723  isrrext  27959  ismntop  27982  issibf  28253  eulerpartleme  28280  eulerpartlemt0  28286  probun  28336  erdszelem1  28613  cvmsval  28689  cvmliftiota  28724  snmlval  28754  lediv2aALT  29021  elwlim  29355  nocvxminlem  29426  nofulllem1  29438  nofulllem5  29442  brtxp2  29507  brpprod3a  29512  brcart  29558  brsuccf  29567  broutsideof3  29752  df3nandALT2  29839  andnand1  29840  fin2solem  30015  itg2gt0cn  30046  iblabsnclem  30054  areacirc  30088  ivthALT  30129  neificl  30222  ablo4pnp  30318  isrngohom  30344  isidl  30387  ispridl  30407  pridlidl  30408  ismaxidl  30413  maxidlidl  30414  isfldidl2  30442  isdmn3  30447  fz1eqin  30678  issdrg  31122  sdrgacs  31126  isdomn3  31140  lcmneg  31185  iotasbc2  31281  stoweidlem17  31753  stoweidlem34  31770  stoweidlem60  31796  ndmaovass  32245  ndmaovdistr  32246  rexdifpr  32254  2elfz3nn0  32286  usgra2pthspth  32305  isrng  32520  2zrngnmrid  32583  lindslinindsimp2lem5  32933  alimp-no-surprise  33066  eelT00  33361  eelTTT  33362  eelT11  33364  eelT12  33368  eelTT1  33370  eelT01  33371  eel0T1  33372  uun132  33450  uun132p1  33451  un2122  33455  uunTT1  33458  uunTT1p1  33459  uunTT1p2  33460  uunT11  33461  uunT11p1  33462  uunT11p2  33463  uunT12  33464  uunT12p1  33465  uunT12p2  33466  uunT12p3  33467  uunT12p4  33468  uunT12p5  33469  uun111  33470  uun2221  33478  uun2221p1  33479  uun2221p2  33480  bnj250  33621  bnj255  33625  bnj345  33634  bnj945  33700  bnj1209  33723  bnj1275  33740  bnj543  33819  bnj571  33832  bnj607  33842  bnj882  33852  bnj983  33877  bnj996  33881  bnj1006  33885  bnj1033  33893  bnj1097  33905  bnj1110  33906  bnj1145  33917  bnj1174  33927  bnj1189  33933  bnj1450  33974  bnj1514  33987  islshp  34579  isopos  34780  cvrfval  34868  cvrval  34869  isatl  34899  isat3  34907  islpln5  35134  4atlem11  35208  dalem20  35292  lhpexle3  35611  lhpex2leN  35612  isltrn2N  35719  diclspsn  36796  lcfls1lem  37136  lcfls1N  37137  rp-isfinite6  37582  snhesn  37631