Theorem 3anass 969

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 967	. 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 965

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 967

This theorem is referenced by:  3anrot  970  3anan12  978  anandi3  979  3biant1d  1327  an33rean  1332  3exdistr  1928  r3al  2768  ceqsex2  3005  ceqsex3v  3007  ceqsex4v  3008  ceqsex6v  3009  ceqsex8v  3010  2reu5lem1  3159  2reu5lem2  3160  2reu5lem3  3161  eldifpr  3889  trel3  4388  ordelord  4736  dflim2  4770  dff1o4  5644  ndmovass  6246  ndmovdistr  6247  dflim3  6453  dflim4  6454  mpt2xopovel  6732  dfsmo2  6800  oeeui  7033  ecopovtrn  7195  elixp2  7259  elixp  7262  mptelixpg  7292  zorn2lem7  8663  grothprim  8993  grothtsk  8994  divmuldiv  10023  sup3  10279  dfnn3  10328  prime  10714  eluz2  10859  uzletr  10861  raluz2  10896  elixx1  11301  elixx3g  11305  elioo2  11333  elioo5  11345  elicc4  11354  iccneg  11398  icoshft  11399  difreicc  11409  elfz1  11434  elfz  11435  elfz2  11436  elfz2nn0  11472  elfzm11  11520  elfzo2  11548  elfzo3  11560  lbfzo0  11578  fzind2  11629  zmodid2  11728  swrdvalodm2  12325  swrdvalodm  12326  wrdeqswrdlsw  12335  swrdccatin1  12366  swrdccat  12376  repswswrd  12414  swrdco  12457  2swrd2eqwrdeq  12545  rediv  12612  imdiv  12619  cosmul  13449  bitsval  13612  bitsmod  13624  bitscmp  13626  smueqlem  13678  elgz  13984  xpsfrnel  14493  xpsfrnel2  14495  ismre  14520  mreexexlem4d  14577  iscatd2  14611  isssc  14725  eldmcoa  14925  isdrs  15096  isipodrs  15323  ismhm  15458  mhmpropd  15462  issubm  15466  submacs  15484  issubg  15672  eqglact  15723  eqgid  15724  pgrpsubgsymgbi  15903  isslw  16098  efgsdm  16218  mulgmhm  16306  mulgghm  16307  dmdprd  16468  dprdw  16482  dprdwOLD  16488  subgdmdprd  16519  dmdprdpr  16536  issrg  16597  srglmhm  16622  srgrmhm  16623  isrng  16637  rnglghm  16681  dfrhm2  16796  issubrg3  16871  islmod  16930  lsspropd  17075  islmhm  17085  islbs  17134  lbspropd  17157  isphl  18032  elocv  18068  isobs  18120  ma1repvcl  18356  smadiadetr  18456  istps3OLD  18502  neindisj  18696  lmbrf  18839  hauscmplem  18984  llyi  19053  subislly  19060  uptx  19173  txcn  19174  qtopeu  19264  elmptrab  19375  isfbas  19377  trfil2  19435  flimcls  19533  cnextcn  19614  psmettri2  19860  xmetec  19984  metuel2  20129  ngppropd  20198  bl2ioo  20344  xrtgioo  20358  om1elbas  20579  elpi1  20592  isclm  20611  iscph  20664  tchcph  20727  lmmbr2  20745  lmmbrf  20748  iscau2  20763  caussi  20783  lmclim  20788  bcthlem1  20810  srabn  20847  ishl2  20857  evthicc2  20919  ovolfioo  20926  ovolficc  20927  iblcnlem1  21240  iblrelem  21243  iblre  21246  iblcn  21251  isuc1p  21587  ismon1p  21589  ellogrn  21986  logreclem  22189  atandm  22246  atandm2  22247  atandm3  22248  atans2  22301  dmarea  22326  dchrelbas4  22557  ax5seg  23135  eengtrkg  23182  nbgrael  23288  nb3grapr2  23313  wlks  23376  wlkon  23380  trls  23386  is2wlk  23415  pths  23416  0pth  23420  isgrpo2  23635  issubgo  23741  ajval  24213  issh  24561  dmadjss  25242  adjeu  25244  adjval  25245  isst  25568  ishst  25569  xrdifh  26021  nndiffz1  26026  xdivpnfrp  26059  isomnd  26115  omndmul2  26126  isslmd  26169  isrrext  26381  issibf  26671  eulerpartleme  26698  eulerpartlemt0  26704  probun  26754  erdszelem1  27031  cvmsval  27107  cvmliftiota  27142  snmlval  27172  lediv2aALT  27273  elwlim  27711  nocvxminlem  27782  nofulllem1  27794  nofulllem5  27798  brtxp2  27863  brpprod3a  27868  brcart  27914  brsuccf  27923  broutsideof3  28108  df3nandALT2  28195  andnand1  28196  fin2solem  28368  itg2gt0cn  28400  iblabsnclem  28408  areacirc  28442  ivthALT  28483  islocfin  28521  neificl  28602  ablo4pnp  28698  isrngohom  28724  isidl  28767  ispridl  28787  pridlidl  28788  ismaxidl  28793  maxidlidl  28794  isfldidl2  28822  isdmn3  28827  fz1eqin  29060  issdrg  29507  sdrgacs  29511  isdomn3  29525  iotasbc2  29627  stoweidlem17  29765  stoweidlem34  29782  stoweidlem60  29808  ndmaovass  30065  ndmaovdistr  30066  rexdifpr  30077  2elfz3nn0  30152  ccats1rev  30213  ccatw2s1p1  30222  ccatw2s1p2  30223  ccat2s1fvw  30224  2wlkeq  30241  usgra2pthspth  30248  usgra2adedgspthlem2  30257  usgra2adedgwlkon  30260  iswwlk  30270  wwlknimp  30274  wwlkextwrd  30313  2pthwlkonot  30357  usg2spthonot  30360  isclwwlk  30384  clwwlknprop  30388  clwwlkn2  30391  clwlkisclwwlklem0  30403  clwlkfclwwlk  30470  isrusgra  30497  rusgranumwlkl1  30512  rusgranumwlklem0  30519  1to3vfriswmgra  30552  numclwwlkovgel  30634  numclwwlk2lem1  30648  mat1dimscm  30794  lindslinindsimp2lem5  30885  alimp-no-surprise  31020  eelT00  31316  eelTTT  31317  eelT11  31319  eelT12  31323  eelTT1  31325  eelT01  31326  eel0T1  31327  uun132  31405  uun132p1  31406  un2122  31410  uunTT1  31413  uunTT1p1  31414  uunTT1p2  31415  uunT11  31416  uunT11p1  31417  uunT11p2  31418  uunT12  31419  uunT12p1  31420  uunT12p2  31421  uunT12p3  31422  uunT12p4  31423  uunT12p5  31424  uun111  31425  uun2221  31433  uun2221p1  31434  uun2221p2  31435  bnj250  31576  bnj255  31580  bnj345  31589  bnj945  31654  bnj1209  31677  bnj1275  31694  bnj543  31773  bnj571  31786  bnj607  31796  bnj882  31806  bnj983  31831  bnj996  31835  bnj1006  31839  bnj1033  31847  bnj1097  31859  bnj1110  31860  bnj1145  31871  bnj1174  31881  bnj1189  31887  bnj1450  31928  bnj1514  31941  islshp  32464  isopos  32665  cvrfval  32753  cvrval  32754  isatl  32784  isat3  32792  islpln5  33019  4atlem11  33093  dalem20  33177  lhpexle3  33496  lhpex2leN  33497  isltrn2N  33604  diclspsn  34679  lcfls1lem  35019  lcfls1N  35020