Theorem 3anass 986

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 984	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 653	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 252	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 187   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  3anrot  987  3anan12  995  anandi3  996  3biant1d  1373  an33rean  1378  cad1  1514  3exdistr  1831  r3alOLD  2870  ceqsex2  3125  ceqsex3v  3127  ceqsex4v  3128  ceqsex6v  3129  ceqsex8v  3130  2reu5lem1  3283  2reu5lem2  3284  2reu5lem3  3285  eldifpr  4019  trel3  4528  ordelord  5464  dflim2  5498  dff1o4  5839  ndmovass  6471  ndmovdistr  6472  dflim3  6688  dflim4  6689  mpt2xopovel  6974  dfsmo2  7074  dfrecs3  7099  oeeui  7311  ecopovtrn  7474  elixp2  7534  elixp  7537  mptelixpg  7567  eqinf  8006  zorn2lem7  8930  grothprim  9258  grothtsk  9259  divmuldiv  10306  sup3  10566  dfnn3  10623  prime  11016  eluz2  11165  raluz2  11208  elixx1  11644  elixx3g  11648  elioo2  11677  elioo5  11692  elicc4  11701  iccneg  11751  icoshft  11752  difreicc  11762  elfz1  11787  elfz  11788  elfz2  11789  elfzm11  11863  elfz2nn0  11883  elfzo2  11921  elfzo3  11934  lbfzo0  11953  fzind2  12020  zmodid2  12122  swrdnd2  12774  swrdccatin1  12824  swrdccat  12834  repswswrd  12872  swrdco  12919  2swrd2eqwrdeq  13007  ccat2s1fvwALT  13009  rediv  13173  imdiv  13180  cosmul  14205  bitsval  14372  bitsmod  14384  bitscmp  14386  smueqlem  14438  lcmneg  14539  lcmftp  14580  coprmgcdb  14625  elgz  14838  xpsfrnel  15420  xpsfrnel2  15422  ismre  15447  mreexexlem4d  15504  iscatd2  15538  isssc  15676  eldmcoa  15911  isdrs  16130  isipodrs  16358  ismhm  16535  mhmpropd  16539  issubm  16545  submacs  16563  issubg  16768  eqglact  16819  eqgid  16820  pgrpsubgsymgbi  16999  isslw  17195  efgsdm  17315  mulgmhm  17403  mulgghm  17404  dmdprd  17565  dprdw  17577  subgdmdprd  17602  dmdprdpr  17617  issrg  17676  srglmhm  17703  srgrmhm  17704  isring  17719  ringlghm  17767  dfrhm2  17880  issubrg3  17971  islmod  18030  lsspropd  18175  islmhm  18185  islbs  18234  lbspropd  18257  isphl  19126  elocv  19162  isobs  19214  mat1dimscm  19431  scmatghm  19489  scmatmhm  19490  ma1repvcl  19526  smadiadetr  19631  mat2pmatghm  19685  mat2pmatmul  19686  decpmatmulsumfsupp  19728  pm2mpghm  19771  pm2mpmhmlem1  19773  neindisj  20064  lmbrf  20207  hauscmplem  20352  llyi  20420  subislly  20427  islocfin  20463  uptx  20571  txcn  20572  qtopeu  20662  elmptrab  20773  isfbas  20775  trfil2  20833  flimcls  20931  cnextcn  21013  xmetec  21380  ngppropd  21576  bl2ioo  21721  xrtgioo  21735  om1elbas  21956  elpi1  21969  isclm  21988  iscph  22041  tchcph  22104  lmmbr2  22122  lmmbrf  22125  iscau2  22140  caussi  22160  lmclim  22165  bcthlem1  22185  srabn  22220  ishl2  22230  evthicc2  22292  ovolfioo  22299  ovolficc  22300  iblcnlem1  22622  iblrelem  22625  iblre  22628  iblcn  22633  isuc1p  22966  ismon1p  22968  ellogrn  23374  logreclem  23564  atandm  23667  atandm2  23668  atandm3  23669  atans2  23722  dmarea  23748  dchrelbas4  24034  ax5seg  24814  eengtrkg  24861  nbgrael  24999  nb3grapr2  25027  wlks  25092  wlkon  25106  trls  25111  is2wlk  25140  pths  25141  0pth  25145  usgra2adedgspthlem2  25185  usgra2adedgwlkon  25188  iswwlk  25256  wwlknimp  25260  2wlkeq  25280  wwlkextwrd  25301  wwlkextinj  25303  isclwwlk  25341  clwwlknprop  25345  clwwlkn2  25348  clwlkisclwwlklem0  25361  clwlkfclwwlk  25417  2pthwlkonot  25458  usg2spthonot  25461  isrusgra  25500  isrusgusrg  25505  isrusgrac  25508  rusgranumwlkl1  25520  rusgranumwlklem0  25521  1to3vfriswmgra  25580  numclwwlkovgel  25661  numclwwlk2lem1  25675  isgrpo2  25770  issubgo  25876  ajval  26348  issh  26696  dmadjss  27375  adjeu  27377  adjval  27378  isst  27701  ishst  27702  xrdifh  28198  nndiffz1  28202  xdivpnfrp  28240  isomnd  28302  isslmd  28356  isrrext  28643  ismntop  28669  isros  28829  issros  28836  issibf  28994  eulerpartleme  29022  eulerpartlemt0  29028  probun  29078  bnj250  29294  bnj255  29298  bnj345  29307  bnj945  29373  bnj1209  29396  bnj1275  29413  bnj543  29492  bnj571  29505  bnj607  29515  bnj882  29525  bnj983  29550  bnj996  29554  bnj1006  29558  bnj1033  29566  bnj1097  29578  bnj1110  29579  bnj1145  29590  bnj1174  29600  bnj1189  29606  bnj1450  29647  bnj1514  29660  erdszelem1  29702  cvmsval  29777  cvmliftiota  29812  snmlval  29842  lediv2aALT  30109  elwlim  30293  nocvxminlem  30364  nofulllem1  30376  nofulllem5  30380  brtxp2  30433  brpprod3a  30438  brcart  30484  brsuccf  30493  broutsideof3  30678  ivthALT  30776  df3nandALT2  30843  andnand1  30844  topdifinffinlem  31484  relowlssretop  31500  fin2solem  31634  poimirlem3  31646  poimirlem4  31647  poimirlem26  31669  poimirlem27  31670  poimirlem32  31675  itg2gt0cn  31700  iblabsnclem  31708  areacirc  31740  neificl  31785  ablo4pnp  31881  isrngohom  31907  isidl  31950  ispridl  31970  pridlidl  31971  ismaxidl  31976  maxidlidl  31977  isfldidl2  32005  isdmn3  32010  islshp  32253  isopos  32454  cvrfval  32542  cvrval  32543  isatl  32573  isat3  32581  islpln5  32808  4atlem11  32882  dalem20  32966  lhpexle3  33285  lhpex2leN  33286  isltrn2N  33393  diclspsn  34470  lcfls1lem  34810  lcfls1N  34811  fz1eqin  35319  issdrg  35761  sdrgacs  35765  isdomn3  35779  rp-isfinite6  35861  snhesn  36018  iotasbc2  36407  eelT00  36723  eelTTT  36724  eelT11  36726  eelT12  36730  eelTT1  36732  eelT01  36733  eel0T1  36734  uun132  36811  uun132p1  36812  un2122  36816  uunTT1  36819  uunTT1p1  36820  uunTT1p2  36821  uunT11  36822  uunT11p1  36823  uunT11p2  36824  uunT12  36825  uunT12p1  36826  uunT12p2  36827  uunT12p3  36828  uunT12p4  36829  uunT12p5  36830  uun111  36831  uun2221  36839  uun2221p1  36840  uun2221p2  36841  stoweidlem17  37445  stoweidlem34  37463  stoweidlem60  37489  ndmaovass  38097  ndmaovdistr  38098  reuccatpfxs1  38364  rexdifpr  38376  2elfz3nn0  38404  usgra2pthspth  38420  isrng  38633  2zrngnmrid  38707  lindslinindsimp2lem5  39014  alimp-no-surprise  39280