Theorem 3anass 1042

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 1039	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 681	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 264	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anrot  1043  3anan12  1051  anandi3  1052  3biant1d  1441  an33rean  1446  cad1  1555  3exdistr  1923  ceqsex2  3244  ceqsex3v  3246  ceqsex4v  3247  ceqsex6v  3248  ceqsex8v  3249  2reu5lem1  3413  2reu5lem2  3414  2reu5lem3  3415  eldifpr  4204  rexdifpr  4205  trel3  4760  2rbropap  5017  ordelord  5745  dflim2  5781  dff1o4  6145  foco2  6379  brfvopab  6700  ndmovass  6822  ndmovdistr  6823  dflim3  7047  dflim4  7048  mpt2xopovel  7346  dfsmo2  7444  dfrecs3  7469  oeeui  7682  ecopovtrn  7850  elixp2  7912  elixp  7915  mptelixpg  7945  eqinf  8390  zorn2lem7  9324  grothprim  9656  grothtsk  9657  divmulasscom  10709  muldivdir  10720  divmuldiv  10725  sup3  10980  dfnn3  11034  prime  11458  eluz2  11693  raluz2  11737  elixx1  12184  elixx3g  12188  elioo2  12216  elioo5  12231  elicc4  12240  iccneg  12293  icoshft  12294  difreicc  12304  elfz1  12331  elfz  12332  elfz2  12333  elfzm11  12411  elfz2nn0  12431  elfzo2  12473  elfzo3  12486  lbfzo0  12507  fzind2  12586  zmodid2  12698  swrdnd2  13433  swrdccatin1  13483  swrdccat  13493  repswswrd  13531  swrdco  13583  2swrd2eqwrdeq  13696  ccat2s1fvwALT  13698  rediv  13871  imdiv  13878  cosmul  14903  bitsval  15146  bitsmod  15158  bitscmp  15160  smueqlem  15212  dfgcd2  15263  lcmneg  15316  lcmftp  15349  coprmgcdb  15362  divgcdcoprmex  15380  cncongr1  15381  cncongr2  15382  difsqpwdvds  15591  oddprmdvds  15607  elgz  15635  xpsfrnel  16223  xpsfrnel2  16225  ismre  16250  mreexexlem4d  16307  iscatd2  16342  isssc  16480  eldmcoa  16715  isdrs  16934  isipodrs  17161  ismhm  17337  mhmpropd  17341  issubm  17347  submacs  17365  issubg  17594  eqglact  17645  eqgid  17646  pgrpsubgsymgbi  17827  isslw  18023  efgsdm  18143  mulgmhm  18233  mulgghm  18234  dmdprd  18397  dprdw  18409  subgdmdprd  18433  dmdprdpr  18448  issrg  18507  srglmhm  18535  srgrmhm  18536  isring  18551  ringlghm  18604  dfrhm2  18717  issubrg3  18808  islmod  18867  lsspropd  19017  islmhm  19027  islbs  19076  lbspropd  19099  isphl  19973  elocv  20012  isobs  20064  mat1dimscm  20281  scmatghm  20339  scmatmhm  20340  ma1repvcl  20376  smadiadetr  20481  mat2pmatghm  20535  mat2pmatmul  20536  decpmatmulsumfsupp  20578  pm2mpghm  20621  pm2mpmhmlem1  20623  neindisj  20921  lmbrf  21064  hauscmplem  21209  llyi  21277  subislly  21284  islocfin  21320  uptx  21428  txcn  21429  qtopeu  21519  elmptrab  21630  isfbas  21633  trfil2  21691  flimcls  21789  cnextcn  21871  xmetec  22239  ngppropd  22441  ngpocelbl  22508  bl2ioo  22595  xrtgioo  22609  om1elbas  22832  elpi1  22845  isclm  22864  isclmp  22897  isncvsngp  22949  iscph  22970  tchcph  23036  lmmbr2  23057  lmmbrf  23060  iscau2  23075  caussi  23095  lmclim  23101  bcthlem1  23121  srabn  23156  ishl2  23166  evthicc2  23229  ovolfioo  23236  ovolficc  23237  iblcnlem1  23554  iblrelem  23557  iblre  23560  iblcn  23565  isuc1p  23900  ismon1p  23902  ellogrn  24306  logreclem  24500  atandm  24603  atandm2  24604  atandm3  24605  atans2  24658  dmarea  24684  dchrelbas4  24968  lgsmodeq  25067  lgsmulsqcoprm  25068  ax5seg  25818  eengtrkg  25865  uspgredg2v  26116  nbgrel  26238  nb3grpr2  26285  isrusgr0  26462  rusgrprop0  26463  ewlkprop  26499  wksfval  26505  wlkeq  26529  wlkson  26552  wlkonprop  26554  upgr2wlk  26564  upgrtrls  26598  upgristrl  26599  wksonproplem  26601  pthsfval  26617  ispth  26619  isspthonpth  26645  uhgrwkspth  26651  usgr2wlkspth  26655  crctcshwlkn0lem4  26705  wspthnp  26737  wwlknon  26742  wwlksnextwrd  26792  wwlksnextinj  26794  wspthsnwspthsnon  26811  umgr2adedgwlk  26841  umgr2adedgwlkon  26842  umgr2adedgwlkonALT  26843  umgr2adedgspth  26844  s3wwlks2on  26849  wpthswwlks2on  26854  usgr2wspthons3  26857  usgr2wspthon  26858  elwwlks2  26861  elwspths2spth  26862  rusgrnumwwlkl1  26863  rusgrnumwwlkslem  26864  isclwwlks  26880  clwwlkbp  26883  clwwlknp  26887  isclwwlksnx  26889  clwlkclwwlklem3  26902  clwwlksn2  26910  clwlksfclwwlk  26962  0pth  26986  frcond4  27134  1to3vfriswmgr  27144  3cyclfrgr  27152  frgrwopreglem5  27185  numclwwlkovgel  27221  numclwwlk6  27248  ajval  27717  issh  28065  dmadjss  28746  adjeu  28748  adjval  28749  isst  29072  ishst  29073  xrdifh  29542  nndiffz1  29548  xdivpnfrp  29641  isomnd  29701  isslmd  29755  isrrext  30044  ismntop  30070  isros  30231  issros  30238  issibf  30395  eulerpartleme  30425  eulerpartlemt0  30431  probun  30481  bnj250  30767  bnj255  30771  bnj345  30780  bnj945  30844  bnj1209  30867  bnj1275  30884  bnj543  30963  bnj571  30976  bnj607  30986  bnj882  30996  bnj983  31021  bnj996  31025  bnj1006  31029  bnj1033  31037  bnj1097  31049  bnj1110  31050  bnj1145  31061  bnj1174  31071  bnj1189  31077  bnj1450  31118  bnj1514  31131  erdszelem1  31173  cvmsval  31248  cvmliftiota  31283  snmlval  31313  lediv2aALT  31571  elwlim  31769  elwlimOLD  31770  nocvxminlem  31893  scutcut  31912  scutbday  31913  brtxp2  31988  brpprod3a  31993  brcart  32039  brsuccf  32048  broutsideof3  32233  ivthALT  32330  df3nandALT2  32397  andnand1  32398  topdifinffinlem  33195  relowlssretop  33211  rdgeqoa  33218  unccur  33392  fin2solem  33395  poimirlem3  33412  poimirlem4  33413  poimirlem26  33435  poimirlem27  33436  poimirlem32  33441  itg2gt0cn  33465  iblabsnclem  33473  areacirc  33505  neificl  33549  ablo4pnp  33679  isrngohom  33764  isidl  33813  ispridl  33833  pridlidl  33834  ismaxidl  33839  maxidlidl  33840  isfldidl2  33868  isdmn3  33873  triantru3  34000  eldmqsres  34051  motr  34127  islshp  34266  isopos  34467  cvrfval  34555  cvrval  34556  isatl  34586  isat3  34594  islpln5  34821  4atlem11  34895  dalem20  34979  lhpexle3  35298  lhpex2leN  35299  isltrn2N  35406  diclspsn  36483  lcfls1lem  36823  lcfls1N  36824  fz1eqin  37332  issdrg  37767  sdrgacs  37771  isdomn3  37782  rp-isfinite6  37864  snhesn  38080  iotasbc2  38621  eelT00  38930  eelTTT  38931  eelT11  38932  eelT12  38934  eelTT1  38935  eelT01  38936  eel0T1  38937  uun132  39012  uun132p1  39013  un2122  39017  uunTT1  39020  uunTT1p1  39021  uunTT1p2  39022  uunT11  39023  uunT11p1  39024  uunT11p2  39025  uunT12  39026  uunT12p1  39027  uunT12p2  39028  uunT12p3  39029  uunT12p4  39030  uunT12p5  39031  uun111  39032  uun2221  39040  uun2221p1  39041  uun2221p2  39042  stoweidlem17  40234  stoweidlem34  40251  stoweidlem60  40277  ndmaovass  41286  ndmaovdistr  41287  2elfz3nn0  41326  reuccatpfxs1  41434  upwlksfval  41716  isupwlkg  41718  upwlkbprop  41719  isrng  41876  2zrngnmrid  41950  lindslinindsimp2lem5  42251  elpg  42457  alimp-no-surprise  42527