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  1512  3exdistr  1832  r3alOLD  2798  ceqsex2  3056  ceqsex3v  3058  ceqsex4v  3059  ceqsex6v  3060  ceqsex8v  3061  2reu5lem1  3215  2reu5lem2  3216  2reu5lem3  3217  eldifpr  3958  trel3  4464  ordelord  5402  dflim2  5436  dff1o4  5777  ndmovass  6410  ndmovdistr  6411  dflim3  6627  dflim4  6628  mpt2xopovel  6916  dfsmo2  7016  dfrecs3  7041  oeeui  7253  ecopovtrn  7416  elixp2  7476  elixp  7479  mptelixpg  7509  eqinf  7948  zorn2lem7  8878  grothprim  9205  grothtsk  9206  divmuldiv  10253  sup3  10512  dfnn3  10569  prime  10962  eluz2  11111  raluz2  11154  elixx1  11590  elixx3g  11594  elioo2  11623  elioo5  11638  elicc4  11647  iccneg  11699  icoshft  11700  difreicc  11710  elfz1  11735  elfz  11736  elfz2  11737  elfzm11  11811  elfz2nn0  11831  elfzo2  11869  elfzo3  11882  lbfzo0  11901  fzind2  11968  zmodid2  12070  swrdnd2  12730  swrdccatin1  12780  swrdccat  12790  repswswrd  12828  swrdco  12875  2swrd2eqwrdeq  12967  ccat2s1fvwALT  12969  rediv  13133  imdiv  13140  cosmul  14165  bitsval  14335  bitsmod  14348  bitscmp  14350  smueqlem  14402  lcmneg  14506  lcmftp  14547  coprmgcdb  14592  elgz  14813  xpsfrnel  15407  xpsfrnel2  15409  ismre  15434  mreexexlem4d  15491  iscatd2  15525  isssc  15663  eldmcoa  15898  isdrs  16117  isipodrs  16345  ismhm  16522  mhmpropd  16526  issubm  16532  submacs  16550  issubg  16755  eqglact  16806  eqgid  16807  pgrpsubgsymgbi  16986  isslw  17198  efgsdm  17318  mulgmhm  17406  mulgghm  17407  dmdprd  17568  dprdw  17580  subgdmdprd  17605  dmdprdpr  17620  issrg  17679  srglmhm  17706  srgrmhm  17707  isring  17722  ringlghm  17770  dfrhm2  17883  issubrg3  17974  islmod  18033  lsspropd  18178  islmhm  18188  islbs  18237  lbspropd  18260  isphl  19132  elocv  19168  isobs  19220  mat1dimscm  19437  scmatghm  19495  scmatmhm  19496  ma1repvcl  19532  smadiadetr  19637  mat2pmatghm  19691  mat2pmatmul  19692  decpmatmulsumfsupp  19734  pm2mpghm  19777  pm2mpmhmlem1  19779  neindisj  20070  lmbrf  20213  hauscmplem  20358  llyi  20426  subislly  20433  islocfin  20469  uptx  20577  txcn  20578  qtopeu  20668  elmptrab  20779  isfbas  20781  trfil2  20839  flimcls  20937  cnextcn  21019  xmetec  21386  ngppropd  21582  bl2ioo  21747  xrtgioo  21761  om1elbas  22000  elpi1  22013  isclm  22032  iscph  22085  tchcph  22148  lmmbr2  22166  lmmbrf  22169  iscau2  22184  caussi  22204  lmclim  22209  bcthlem1  22229  srabn  22264  ishl2  22274  evthicc2  22348  ovolfioo  22357  ovolficc  22358  iblcnlem1  22682  iblrelem  22685  iblre  22688  iblcn  22693  isuc1p  23028  ismon1p  23030  ellogrn  23446  logreclem  23636  atandm  23739  atandm2  23740  atandm3  23741  atans2  23794  dmarea  23820  dchrelbas4  24108  ax5seg  24905  eengtrkg  24952  nbgrael  25091  nb3grapr2  25119  wlks  25184  wlkon  25198  trls  25203  is2wlk  25232  pths  25233  0pth  25237  usgra2adedgspthlem2  25277  usgra2adedgwlkon  25280  iswwlk  25348  wwlknimp  25352  2wlkeq  25372  wwlkextwrd  25393  wwlkextinj  25395  isclwwlk  25433  clwwlknprop  25437  clwwlkn2  25440  clwlkisclwwlklem0  25453  clwlkfclwwlk  25509  2pthwlkonot  25550  usg2spthonot  25553  isrusgra  25592  isrusgusrg  25597  isrusgrac  25600  rusgranumwlkl1  25612  rusgranumwlklem0  25613  1to3vfriswmgra  25672  numclwwlkovgel  25753  numclwwlk2lem1  25767  isgrpo2  25862  issubgo  25968  ajval  26440  issh  26798  dmadjss  27477  adjeu  27479  adjval  27480  isst  27803  ishst  27804  xrdifh  28307  nndiffz1  28311  xdivpnfrp  28348  isomnd  28410  isslmd  28464  isrrext  28751  ismntop  28777  isros  28937  issros  28944  issibf  29113  eulerpartleme  29143  eulerpartlemt0  29149  probun  29199  bnj250  29453  bnj255  29457  bnj345  29466  bnj945  29532  bnj1209  29555  bnj1275  29572  bnj543  29651  bnj571  29664  bnj607  29674  bnj882  29684  bnj983  29709  bnj996  29713  bnj1006  29717  bnj1033  29725  bnj1097  29737  bnj1110  29738  bnj1145  29749  bnj1174  29759  bnj1189  29765  bnj1450  29806  bnj1514  29819  erdszelem1  29861  cvmsval  29936  cvmliftiota  29971  snmlval  30001  lediv2aALT  30268  elwlim  30452  nocvxminlem  30523  nofulllem1  30535  nofulllem5  30539  brtxp2  30592  brpprod3a  30597  brcart  30643  brsuccf  30652  broutsideof3  30837  ivthALT  30935  df3nandALT2  31002  andnand1  31003  topdifinffinlem  31657  relowlssretop  31673  rdgeqoa  31680  fin2solem  31838  poimirlem3  31850  poimirlem4  31851  poimirlem26  31873  poimirlem27  31874  poimirlem32  31879  itg2gt0cn  31904  iblabsnclem  31912  areacirc  31944  neificl  31989  ablo4pnp  32085  isrngohom  32111  isidl  32154  ispridl  32174  pridlidl  32175  ismaxidl  32180  maxidlidl  32181  isfldidl2  32209  isdmn3  32214  islshp  32457  isopos  32658  cvrfval  32746  cvrval  32747  isatl  32777  isat3  32785  islpln5  33012  4atlem11  33086  dalem20  33170  lhpexle3  33489  lhpex2leN  33490  isltrn2N  33597  diclspsn  34674  lcfls1lem  35014  lcfls1N  35015  fz1eqin  35523  issdrg  35976  sdrgacs  35980  isdomn3  35994  rp-isfinite6  36076  snhesn  36295  iotasbc2  36684  eelT00  37000  eelTTT  37001  eelT11  37003  eelT12  37007  eelTT1  37009  eelT01  37010  eel0T1  37011  uun132  37088  uun132p1  37089  un2122  37093  uunTT1  37096  uunTT1p1  37097  uunTT1p2  37098  uunT11  37099  uunT11p1  37100  uunT11p2  37101  uunT12  37102  uunT12p1  37103  uunT12p2  37104  uunT12p3  37105  uunT12p4  37106  uunT12p5  37107  uun111  37108  uun2221  37116  uun2221p1  37117  uun2221p2  37118  stoweidlem17  37760  stoweidlem34  37778  stoweidlem60  37804  ndmaovass  38521  ndmaovdistr  38522  reuccatpfxs1  38788  rexdifpr  38803  2elfz3nn0  38853  nbgrel  39146  nb3grpr2  39188  usgra2pthspth  39256  isrng  39467  2zrngnmrid  39541  lindslinindsimp2lem5  39848  alimp-no-surprise  40113