Theorem 3anass 962

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 960	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 642	. 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 958

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 960

This theorem is referenced by:  3anrot  963  3anan12  971  anandi3  972  3biant1d  1320  an33rean  1325  3exdistr  1927  r3al  2763  ceqsex2  2999  ceqsex3v  3001  ceqsex4v  3002  ceqsex6v  3003  ceqsex8v  3004  2reu5lem1  3153  2reu5lem2  3154  2reu5lem3  3155  eldifpr  3882  trel3  4381  ordelord  4728  dflim2  4762  dff1o4  5637  ndmovass  6240  ndmovdistr  6241  dflim3  6447  dflim4  6448  mpt2xopovel  6726  dfsmo2  6794  oeeui  7029  ecopovtrn  7191  elixp2  7255  elixp  7258  mptelixpg  7288  zorn2lem7  8659  grothprim  8988  grothtsk  8989  divmuldiv  10018  sup3  10274  dfnn3  10323  prime  10709  eluz2  10854  uzletr  10856  raluz2  10891  elixx1  11296  elixx3g  11300  elioo2  11328  elioo5  11340  elicc4  11349  iccneg  11392  icoshft  11393  difreicc  11403  elfz1  11428  elfz  11429  elfz2  11430  elfz2nn0  11466  elfzm11  11511  elfzo2  11539  elfzo3  11551  lbfzo0  11569  fzind2  11620  zmodid2  11719  swrdvalodm2  12316  swrdvalodm  12317  wrdeqswrdlsw  12326  swrdccatin1  12357  swrdccat  12367  repswswrd  12405  swrdco  12448  2swrd2eqwrdeq  12536  rediv  12603  imdiv  12610  cosmul  13439  bitsval  13602  bitsmod  13614  bitscmp  13616  smueqlem  13668  elgz  13974  xpsfrnel  14483  xpsfrnel2  14485  ismre  14510  mreexexlem4d  14567  iscatd2  14601  isssc  14715  eldmcoa  14915  isdrs  15086  isipodrs  15313  ismhm  15448  mhmpropd  15452  issubm  15456  submacs  15474  issubg  15660  eqglact  15711  eqgid  15712  pgrpsubgsymgbi  15891  isslw  16086  efgsdm  16206  mulgmhm  16294  mulgghm  16295  dmdprd  16453  dprdw  16467  dprdwOLD  16473  subgdmdprd  16504  dmdprdpr  16521  isrng  16584  rnglghm  16627  dfrhm2  16741  issubrg3  16816  islmod  16875  lsspropd  17019  islmhm  17029  islbs  17078  lbspropd  17101  isphl  17898  elocv  17934  isobs  17986  ma1repvcl  18222  smadiadetr  18322  istps3OLD  18368  neindisj  18562  lmbrf  18705  hauscmplem  18850  llyi  18919  subislly  18926  uptx  19039  txcn  19040  qtopeu  19130  elmptrab  19241  isfbas  19243  trfil2  19301  flimcls  19399  cnextcn  19480  psmettri2  19726  xmetec  19850  metuel2  19995  ngppropd  20064  bl2ioo  20210  xrtgioo  20224  om1elbas  20445  elpi1  20458  isclm  20477  iscph  20530  tchcph  20593  lmmbr2  20611  lmmbrf  20614  iscau2  20629  caussi  20649  lmclim  20654  bcthlem1  20676  srabn  20713  ishl2  20723  evthicc2  20785  ovolfioo  20792  ovolficc  20793  iblcnlem1  21106  iblrelem  21109  iblre  21112  iblcn  21117  isuc1p  21496  ismon1p  21498  ellogrn  21895  logreclem  22098  atandm  22155  atandm2  22156  atandm3  22157  atans2  22210  dmarea  22235  dchrelbas4  22466  ax5seg  23006  eengtrkg  23053  nbgrael  23159  nb3grapr2  23184  wlks  23247  wlkon  23251  trls  23257  is2wlk  23286  pths  23287  0pth  23291  isgrpo2  23506  issubgo  23612  ajval  24084  issh  24432  dmadjss  25113  adjeu  25115  adjval  25116  isst  25439  ishst  25440  xrdifh  25892  nndiffz1  25897  xdivpnfrp  25930  isomnd  25987  omndmul2  25998  issrg  26041  isslmd  26066  isrrext  26282  issibf  26566  eulerpartleme  26593  eulerpartlemt0  26599  probun  26649  erdszelem1  26926  cvmsval  27002  cvmliftiota  27037  snmlval  27067  lediv2aALT  27168  elwlim  27606  nocvxminlem  27677  nofulllem1  27689  nofulllem5  27693  brtxp2  27758  brpprod3a  27763  brcart  27809  brsuccf  27818  broutsideof3  28003  df3nandALT2  28090  andnand1  28091  fin2solem  28256  itg2gt0cn  28288  iblabsnclem  28296  areacirc  28330  ivthALT  28371  islocfin  28409  neificl  28490  ablo4pnp  28586  isrngohom  28612  isidl  28655  ispridl  28675  pridlidl  28676  ismaxidl  28681  maxidlidl  28682  isfldidl2  28710  isdmn3  28715  fz1eqin  28949  issdrg  29396  sdrgacs  29400  isdomn3  29414  iotasbc2  29516  stoweidlem17  29655  stoweidlem34  29672  stoweidlem60  29698  ndmaovass  29955  ndmaovdistr  29956  rexdifpr  29967  2elfz3nn0  30042  ccats1rev  30103  ccatw2s1p1  30112  ccatw2s1p2  30113  ccat2s1fvw  30114  2wlkeq  30131  usgra2pthspth  30138  usgra2adedgspthlem2  30147  usgra2adedgwlkon  30150  iswwlk  30160  wwlknimp  30164  wwlkextwrd  30203  2pthwlkonot  30247  usg2spthonot  30250  isclwwlk  30274  clwwlknprop  30278  clwwlkn2  30281  clwlkisclwwlklem0  30293  clwlkfclwwlk  30360  isrusgra  30387  rusgranumwlkl1  30402  rusgranumwlklem0  30409  1to3vfriswmgra  30442  numclwwlkovgel  30524  numclwwlk2lem1  30538  lindslinindsimp2lem5  30702  alimp-no-surprise  30837  eelT00  31128  eelTTT  31129  eelT11  31131  eelT12  31135  eelTT1  31137  eelT01  31138  eel0T1  31139  uun132  31217  uun132p1  31218  un2122  31222  uunTT1  31225  uunTT1p1  31226  uunTT1p2  31227  uunT11  31228  uunT11p1  31229  uunT11p2  31230  uunT12  31231  uunT12p1  31232  uunT12p2  31233  uunT12p3  31234  uunT12p4  31235  uunT12p5  31236  uun111  31237  uun2221  31245  uun2221p1  31246  uun2221p2  31247  bnj250  31388  bnj255  31392  bnj345  31401  bnj945  31466  bnj1209  31489  bnj1275  31506  bnj543  31585  bnj571  31598  bnj607  31608  bnj882  31618  bnj983  31643  bnj996  31647  bnj1006  31651  bnj1033  31659  bnj1097  31671  bnj1110  31672  bnj1145  31683  bnj1174  31693  bnj1189  31699  bnj1450  31740  bnj1514  31753  islshp  32194  isopos  32395  cvrfval  32483  cvrval  32484  isatl  32514  isat3  32522  islpln5  32749  4atlem11  32823  dalem20  32907  lhpexle3  33226  lhpex2leN  33227  isltrn2N  33334  diclspsn  34409  lcfls1lem  34749  lcfls1N  34750