Theorem 3anass 975

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 973	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 647	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 249	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 184   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  3anrot  976  3anan12  984  anandi3  985  3biant1d  1335  an33rean  1340  cad1  1472  3exdistr  1788  r3alOLD  2820  ceqsex2  3072  ceqsex3v  3074  ceqsex4v  3075  ceqsex6v  3076  ceqsex8v  3077  2reu5lem1  3230  2reu5lem2  3231  2reu5lem3  3232  eldifpr  3961  trel3  4468  ordelord  4814  dflim2  4848  dff1o4  5732  ndmovass  6362  ndmovdistr  6363  dflim3  6581  dflim4  6582  mpt2xopovel  6866  dfsmo2  6936  oeeui  7169  ecopovtrn  7332  elixp2  7392  elixp  7395  mptelixpg  7425  zorn2lem7  8795  grothprim  9123  grothtsk  9124  divmuldiv  10161  sup3  10416  dfnn3  10466  prime  10860  eluz2  11007  raluz2  11050  elixx1  11459  elixx3g  11463  elioo2  11491  elioo5  11503  elicc4  11512  iccneg  11562  icoshft  11563  difreicc  11573  elfz1  11598  elfz  11599  elfz2  11600  elfzm11  11671  elfz2nn0  11691  elfzo2  11725  elfzo3  11738  lbfzo0  11757  fzind2  11823  zmodid2  11925  swrdnd2  12569  swrdccatin1  12619  swrdccat  12629  repswswrd  12667  swrdco  12714  2swrd2eqwrdeq  12802  ccat2s1fvwALT  12804  rediv  12966  imdiv  12973  cosmul  13910  bitsval  14076  bitsmod  14088  bitscmp  14090  smueqlem  14142  elgz  14451  xpsfrnel  14970  xpsfrnel2  14972  ismre  14997  mreexexlem4d  15054  iscatd2  15088  isssc  15226  eldmcoa  15461  isdrs  15680  isipodrs  15908  ismhm  16085  mhmpropd  16089  issubm  16095  submacs  16113  issubg  16318  eqglact  16369  eqgid  16370  pgrpsubgsymgbi  16549  isslw  16745  efgsdm  16865  mulgmhm  16953  mulgghm  16954  dmdprd  17142  dprdw  17156  dprdwOLD  17163  subgdmdprd  17194  dmdprdpr  17211  issrg  17272  srglmhm  17299  srgrmhm  17300  isring  17315  ringlghm  17363  dfrhm2  17479  issubrg3  17570  islmod  17629  lsspropd  17776  islmhm  17786  islbs  17835  lbspropd  17858  isphl  18754  elocv  18790  isobs  18842  mat1dimscm  19062  scmatghm  19120  scmatmhm  19121  ma1repvcl  19157  smadiadetr  19262  mat2pmatghm  19316  mat2pmatmul  19317  decpmatmulsumfsupp  19359  pm2mpghm  19402  pm2mpmhmlem1  19404  istps3OLD  19508  neindisj  19704  lmbrf  19847  hauscmplem  19992  llyi  20060  subislly  20067  islocfin  20103  uptx  20211  txcn  20212  qtopeu  20302  elmptrab  20413  isfbas  20415  trfil2  20473  flimcls  20571  cnextcn  20652  xmetec  21022  ngppropd  21236  bl2ioo  21382  xrtgioo  21396  om1elbas  21617  elpi1  21630  isclm  21649  iscph  21702  tchcph  21765  lmmbr2  21783  lmmbrf  21786  iscau2  21801  caussi  21821  lmclim  21826  bcthlem1  21848  srabn  21885  ishl2  21895  evthicc2  21957  ovolfioo  21964  ovolficc  21965  iblcnlem1  22279  iblrelem  22282  iblre  22285  iblcn  22290  isuc1p  22626  ismon1p  22628  ellogrn  23032  logreclem  23220  atandm  23323  atandm2  23324  atandm3  23325  atans2  23378  dmarea  23404  dchrelbas4  23635  ax5seg  24362  eengtrkg  24409  nbgrael  24547  nb3grapr2  24575  wlks  24640  wlkon  24654  trls  24659  is2wlk  24688  pths  24689  0pth  24693  usgra2adedgspthlem2  24733  usgra2adedgwlkon  24736  iswwlk  24804  wwlknimp  24808  2wlkeq  24828  wwlkextwrd  24849  wwlkextinj  24851  isclwwlk  24889  clwwlknprop  24893  clwwlkn2  24896  clwlkisclwwlklem0  24909  clwlkfclwwlk  24965  2pthwlkonot  25006  usg2spthonot  25009  isrusgra  25048  isrusgusrg  25053  isrusgrac  25056  rusgranumwlkl1  25068  rusgranumwlklem0  25069  1to3vfriswmgra  25128  numclwwlkovgel  25209  numclwwlk2lem1  25223  isgrpo2  25316  issubgo  25422  ajval  25894  issh  26242  dmadjss  26922  adjeu  26924  adjval  26925  isst  27248  ishst  27249  xrdifh  27744  nndiffz1  27749  xdivpnfrp  27782  isomnd  27844  isslmd  27898  isrrext  28134  ismntop  28157  issibf  28458  eulerpartleme  28485  eulerpartlemt0  28491  probun  28541  erdszelem1  28824  cvmsval  28900  cvmliftiota  28935  snmlval  28965  lediv2aALT  29232  elwlim  29544  nocvxminlem  29615  nofulllem1  29627  nofulllem5  29631  brtxp2  29684  brpprod3a  29689  brcart  29735  brsuccf  29744  broutsideof3  29929  df3nandALT2  30016  andnand1  30017  fin2solem  30204  itg2gt0cn  30236  iblabsnclem  30244  areacirc  30278  ivthALT  30319  neificl  30412  ablo4pnp  30508  isrngohom  30534  isidl  30577  ispridl  30597  pridlidl  30598  ismaxidl  30603  maxidlidl  30604  isfldidl2  30632  isdmn3  30637  fz1eqin  30867  issdrg  31314  sdrgacs  31318  isdomn3  31332  lcmneg  31377  iotasbc2  31495  stoweidlem17  31965  stoweidlem34  31982  stoweidlem60  32008  ndmaovass  32457  ndmaovdistr  32458  reuccatpfxs1  32609  rexdifpr  32621  2elfz3nn0  32653  usgra2pthspth  32669  isrng  32882  2zrngnmrid  32956  lindslinindsimp2lem5  33263  alimp-no-surprise  33530  eelT00  33833  eelTTT  33834  eelT11  33836  eelT12  33840  eelTT1  33842  eelT01  33843  eel0T1  33844  uun132  33922  uun132p1  33923  un2122  33927  uunTT1  33930  uunTT1p1  33931  uunTT1p2  33932  uunT11  33933  uunT11p1  33934  uunT11p2  33935  uunT12  33936  uunT12p1  33937  uunT12p2  33938  uunT12p3  33939  uunT12p4  33940  uunT12p5  33941  uun111  33942  uun2221  33950  uun2221p1  33951  uun2221p2  33952  bnj250  34100  bnj255  34104  bnj345  34113  bnj945  34179  bnj1209  34202  bnj1275  34219  bnj543  34298  bnj571  34311  bnj607  34321  bnj882  34331  bnj983  34356  bnj996  34360  bnj1006  34364  bnj1033  34372  bnj1097  34384  bnj1110  34385  bnj1145  34396  bnj1174  34406  bnj1189  34412  bnj1450  34453  bnj1514  34466  islshp  35117  isopos  35318  cvrfval  35406  cvrval  35407  isatl  35437  isat3  35445  islpln5  35672  4atlem11  35746  dalem20  35830  lhpexle3  36149  lhpex2leN  36150  isltrn2N  36257  diclspsn  37334  lcfls1lem  37674  lcfls1N  37675  rp-isfinite6  38173  snhesn  38281