Theorem 3anass 977

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 975	. 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 973

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 975

This theorem is referenced by:  3anrot  978  3anan12  986  anandi3  987  3biant1d  1337  an33rean  1342  3exdistr  1954  r3alOLD  2902  rsp2e  2923  ceqsex2  3151  ceqsex3v  3153  ceqsex4v  3154  ceqsex6v  3155  ceqsex8v  3156  2reu5lem1  3309  2reu5lem2  3310  2reu5lem3  3311  eldifpr  4044  trel3  4548  ordelord  4900  dflim2  4934  dff1o4  5823  ndmovass  6446  ndmovdistr  6447  dflim3  6661  dflim4  6662  mpt2xopovel  6948  dfsmo2  7018  oeeui  7251  ecopovtrn  7414  elixp2  7473  elixp  7476  mptelixpg  7506  zorn2lem7  8881  grothprim  9211  grothtsk  9212  divmuldiv  10243  sup3  10499  dfnn3  10549  prime  10940  eluz2  11087  raluz2  11129  elixx1  11537  elixx3g  11541  elioo2  11569  elioo5  11581  elicc4  11590  iccneg  11640  icoshft  11641  difreicc  11651  elfz1  11676  elfz  11677  elfz2  11678  elfzm11  11748  elfz2nn0  11767  elfzo2  11799  elfzo3  11811  lbfzo0  11829  fzind2  11891  zmodid2  11991  ccatw2s1p1  12602  ccatw2s1p2  12603  swrdvalodm2  12626  swrdvalodm  12627  wrdeqswrdlsw  12636  swrdccatin1  12670  swrdccat  12680  repswswrd  12718  swrdco  12765  2swrd2eqwrdeq  12853  ccat2s1fvwALT  12855  rediv  12926  imdiv  12933  cosmul  13768  bitsval  13932  bitsmod  13944  bitscmp  13946  smueqlem  13998  elgz  14307  xpsfrnel  14817  xpsfrnel2  14819  ismre  14844  mreexexlem4d  14901  iscatd2  14935  isssc  15049  eldmcoa  15249  isdrs  15420  isipodrs  15647  ismhm  15785  mhmpropd  15789  issubm  15794  submacs  15812  issubg  16003  eqglact  16054  eqgid  16055  pgrpsubgsymgbi  16234  isslw  16431  efgsdm  16551  mulgmhm  16639  mulgghm  16640  dmdprd  16829  dprdw  16843  dprdwOLD  16849  subgdmdprd  16880  dmdprdpr  16897  issrg  16958  srglmhm  16983  srgrmhm  16984  isrng  16999  rnglghm  17046  dfrhm2  17162  issubrg3  17252  islmod  17311  lsspropd  17458  islmhm  17468  islbs  17517  lbspropd  17540  isphl  18446  elocv  18482  isobs  18534  mat1dimscm  18760  scmatghm  18818  scmatmhm  18819  ma1repvcl  18855  smadiadetr  18960  mat2pmatghm  19014  mat2pmatmul  19015  decpmatmulsumfsupp  19057  pm2mpghm  19100  pm2mpmhmlem1  19102  istps3OLD  19206  neindisj  19400  lmbrf  19543  hauscmplem  19688  llyi  19757  subislly  19764  uptx  19877  txcn  19878  qtopeu  19968  elmptrab  20079  isfbas  20081  trfil2  20139  flimcls  20237  cnextcn  20318  psmettri2  20564  xmetec  20688  metuel2  20833  ngppropd  20902  bl2ioo  21048  xrtgioo  21062  om1elbas  21283  elpi1  21296  isclm  21315  iscph  21368  tchcph  21431  lmmbr2  21449  lmmbrf  21452  iscau2  21467  caussi  21487  lmclim  21492  bcthlem1  21514  srabn  21551  ishl2  21561  evthicc2  21623  ovolfioo  21630  ovolficc  21631  iblcnlem1  21945  iblrelem  21948  iblre  21951  iblcn  21956  isuc1p  22292  ismon1p  22294  ellogrn  22691  logreclem  22894  atandm  22951  atandm2  22952  atandm3  22953  atans2  23006  dmarea  23031  dchrelbas4  23262  ax5seg  23933  eengtrkg  23980  nbgrael  24118  nb3grapr2  24146  wlks  24211  wlkon  24225  trls  24230  is2wlk  24259  pths  24260  0pth  24264  usgra2adedgspthlem2  24304  usgra2adedgwlkon  24307  iswwlk  24375  wwlknimp  24379  2wlkeq  24399  wwlkextwrd  24420  isclwwlk  24460  clwwlknprop  24464  clwwlkn2  24467  clwlkisclwwlklem0  24480  clwlkfclwwlk  24536  2pthwlkonot  24577  usg2spthonot  24580  isrusgra  24619  isrusgusrg  24624  isrusgrac  24627  rusgranumwlkl1  24639  rusgranumwlklem0  24640  1to3vfriswmgra  24699  numclwwlkovgel  24781  numclwwlk2lem1  24795  isgrpo2  24891  issubgo  24997  ajval  25469  issh  25817  dmadjss  26498  adjeu  26500  adjval  26501  isst  26824  ishst  26825  xrdifh  27275  nndiffz1  27280  xdivpnfrp  27313  isomnd  27369  omndmul2  27380  isslmd  27423  isrrext  27633  ismntop  27660  issibf  27931  eulerpartleme  27958  eulerpartlemt0  27964  probun  28014  erdszelem1  28291  cvmsval  28367  cvmliftiota  28402  snmlval  28432  lediv2aALT  28534  elwlim  28972  nocvxminlem  29043  nofulllem1  29055  nofulllem5  29059  brtxp2  29124  brpprod3a  29129  brcart  29175  brsuccf  29184  broutsideof3  29369  df3nandALT2  29456  andnand1  29457  fin2solem  29632  itg2gt0cn  29663  iblabsnclem  29671  areacirc  29705  ivthALT  29746  islocfin  29784  neificl  29865  ablo4pnp  29961  isrngohom  29987  isidl  30030  ispridl  30050  pridlidl  30051  ismaxidl  30056  maxidlidl  30057  isfldidl2  30085  isdmn3  30090  fz1eqin  30322  issdrg  30767  sdrgacs  30771  isdomn3  30785  lcmneg  30825  iotasbc2  30921  stoweidlem17  31333  stoweidlem34  31350  stoweidlem60  31376  ndmaovass  31774  ndmaovdistr  31775  rexdifpr  31783  2elfz3nn0  31815  usgra2pthspth  31834  isrng0  32001  lindslinindsimp2lem5  32153  alimp-no-surprise  32286  eelT00  32582  eelTTT  32583  eelT11  32585  eelT12  32589  eelTT1  32591  eelT01  32592  eel0T1  32593  uun132  32671  uun132p1  32672  un2122  32676  uunTT1  32679  uunTT1p1  32680  uunTT1p2  32681  uunT11  32682  uunT11p1  32683  uunT11p2  32684  uunT12  32685  uunT12p1  32686  uunT12p2  32687  uunT12p3  32688  uunT12p4  32689  uunT12p5  32690  uun111  32691  uun2221  32699  uun2221p1  32700  uun2221p2  32701  bnj250  32842  bnj255  32846  bnj345  32855  bnj945  32920  bnj1209  32943  bnj1275  32960  bnj543  33039  bnj571  33052  bnj607  33062  bnj882  33072  bnj983  33097  bnj996  33101  bnj1006  33105  bnj1033  33113  bnj1097  33125  bnj1110  33126  bnj1145  33137  bnj1174  33147  bnj1189  33153  bnj1450  33194  bnj1514  33207  islshp  33785  isopos  33986  cvrfval  34074  cvrval  34075  isatl  34105  isat3  34113  islpln5  34340  4atlem11  34414  dalem20  34498  lhpexle3  34817  lhpex2leN  34818  isltrn2N  34925  diclspsn  36000  lcfls1lem  36340  lcfls1N  36341