Theorem 3anass 1035

Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3anass	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Proof of Theorem 3anass

Step	Hyp	Ref	Expression
1		df-3an 1033	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 679	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 263	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anrot  1036  3anan12  1044  anandi3  1045  3biant1d  1433  an33rean  1438  cad1  1546  3exdistr  1910  ceqsex2  3217  ceqsex3v  3219  ceqsex4v  3220  ceqsex6v  3221  ceqsex8v  3222  2reu5lem1  3380  2reu5lem2  3381  2reu5lem3  3382  eldifpr  4152  trel3  4688  2rbropap  4941  ordelord  5662  dflim2  5698  dff1o4  6058  foco2  6287  fvmptopab2  6595  brfvopab  6598  ndmovass  6720  ndmovdistr  6721  dflim3  6939  dflim4  6940  mpt2xopovel  7233  dfsmo2  7331  dfrecs3  7356  oeeui  7569  ecopovtrn  7737  elixp2  7798  elixp  7801  mptelixpg  7831  eqinf  8273  zorn2lem7  9207  grothprim  9535  grothtsk  9536  divmulasscom  10588  muldivdir  10599  divmuldiv  10604  sup3  10859  dfnn3  10911  prime  11334  eluz2  11569  raluz2  11613  elixx1  12055  elixx3g  12059  elioo2  12087  elioo5  12102  elicc4  12111  iccneg  12164  icoshft  12165  difreicc  12175  elfz1  12202  elfz  12203  elfz2  12204  elfzm11  12280  elfz2nn0  12300  elfzo2  12342  elfzo3  12355  lbfzo0  12375  fzind2  12448  zmodid2  12560  swrdnd2  13285  swrdccatin1  13334  swrdccat  13344  repswswrd  13382  swrdco  13434  2swrd2eqwrdeq  13544  ccat2s1fvwALT  13546  rediv  13719  imdiv  13726  cosmul  14742  bitsval  14984  bitsmod  14996  bitscmp  14998  smueqlem  15050  dfgcd2  15101  lcmneg  15154  lcmftp  15187  coprmgcdb  15200  divgcdcoprmex  15218  cncongr1  15219  cncongr2  15220  difsqpwdvds  15429  oddprmdvds  15445  elgz  15473  xpsfrnel  16046  xpsfrnel2  16048  ismre  16073  mreexexlem4d  16130  iscatd2  16165  isssc  16303  eldmcoa  16538  isdrs  16757  isipodrs  16984  ismhm  17160  mhmpropd  17164  issubm  17170  submacs  17188  issubg  17417  eqglact  17468  eqgid  17469  pgrpsubgsymgbi  17650  isslw  17846  efgsdm  17966  mulgmhm  18056  mulgghm  18057  dmdprd  18220  dprdw  18232  subgdmdprd  18256  dmdprdpr  18271  issrg  18330  srglmhm  18358  srgrmhm  18359  isring  18374  ringlghm  18427  dfrhm2  18540  issubrg3  18631  islmod  18690  lsspropd  18838  islmhm  18848  islbs  18897  lbspropd  18920  isphl  19792  elocv  19831  isobs  19883  mat1dimscm  20100  scmatghm  20158  scmatmhm  20159  ma1repvcl  20195  smadiadetr  20300  mat2pmatghm  20354  mat2pmatmul  20355  decpmatmulsumfsupp  20397  pm2mpghm  20440  pm2mpmhmlem1  20442  neindisj  20731  lmbrf  20874  hauscmplem  21019  llyi  21087  subislly  21094  islocfin  21130  uptx  21238  txcn  21239  qtopeu  21329  elmptrab  21440  isfbas  21443  trfil2  21501  flimcls  21599  cnextcn  21681  xmetec  22049  ngppropd  22251  ngpocelbl  22318  bl2ioo  22403  xrtgioo  22417  om1elbas  22640  elpi1  22653  isclm  22672  isclmp  22705  isncvsngp  22757  iscph  22778  tchcph  22844  lmmbr2  22865  lmmbrf  22868  iscau2  22883  caussi  22903  lmclim  22909  bcthlem1  22929  srabn  22964  ishl2  22974  evthicc2  23036  ovolfioo  23043  ovolficc  23044  iblcnlem1  23360  iblrelem  23363  iblre  23366  iblcn  23371  isuc1p  23704  ismon1p  23706  ellogrn  24110  logreclem  24300  atandm  24403  atandm2  24404  atandm3  24405  atans2  24458  dmarea  24484  dchrelbas4  24768  lgsmodeq  24867  lgsmulsqcoprm  24868  ax5seg  25618  eengtrkg  25665  nbgrael  25955  nb3grapr2  25983  wlks  26047  wlkon  26061  trls  26066  is2wlk  26095  pths  26096  0pth  26100  usgra2adedgspthlem2  26140  usgra2adedgwlkon  26143  iswwlk  26211  wwlknimp  26215  2wlkeq  26235  wwlkextwrd  26256  wwlkextinj  26258  isclwwlk  26296  clwwlknprop  26300  clwwlkn2  26303  clwlkisclwwlklem0  26316  clwlkfclwwlk  26371  2pthwlkonot  26412  usg2spthonot  26415  isrusgra  26454  isrusgusrg  26459  isrusgrac  26462  rusgranumwlkl1  26474  rusgranumwlklem0  26475  1to3vfriswmgra  26534  numclwwlkovgel  26615  numclwwlk2lem1  26629  ajval  27101  issh  27449  dmadjss  28130  adjeu  28132  adjval  28133  isst  28456  ishst  28457  xrdifh  28932  nndiffz1  28936  xdivpnfrp  28972  isomnd  29032  isslmd  29086  isrrext  29372  ismntop  29398  isros  29558  issros  29565  issibf  29722  eulerpartleme  29752  eulerpartlemt0  29758  probun  29808  bnj250  30020  bnj255  30024  bnj345  30033  bnj945  30098  bnj1209  30121  bnj1275  30138  bnj543  30217  bnj571  30230  bnj607  30240  bnj882  30250  bnj983  30275  bnj996  30279  bnj1006  30283  bnj1033  30291  bnj1097  30303  bnj1110  30304  bnj1145  30315  bnj1174  30325  bnj1189  30331  bnj1450  30372  bnj1514  30385  erdszelem1  30427  cvmsval  30502  cvmliftiota  30537  snmlval  30567  lediv2aALT  30825  elwlim  31013  elwlimOLD  31014  nocvxminlem  31089  nofulllem1  31101  nofulllem5  31105  brtxp2  31158  brpprod3a  31163  brcart  31209  brsuccf  31218  broutsideof3  31403  ivthALT  31500  df3nandALT2  31567  andnand1  31568  topdifinffinlem  32371  relowlssretop  32387  rdgeqoa  32394  unccur  32562  fin2solem  32565  poimirlem3  32582  poimirlem4  32583  poimirlem26  32605  poimirlem27  32606  poimirlem32  32611  itg2gt0cn  32635  iblabsnclem  32643  areacirc  32675  neificl  32719  ablo4pnp  32849  isrngohom  32934  isidl  32983  ispridl  33003  pridlidl  33004  ismaxidl  33009  maxidlidl  33010  isfldidl2  33038  isdmn3  33043  islshp  33284  isopos  33485  cvrfval  33573  cvrval  33574  isatl  33604  isat3  33612  islpln5  33839  4atlem11  33913  dalem20  33997  lhpexle3  34316  lhpex2leN  34317  isltrn2N  34424  diclspsn  35501  lcfls1lem  35841  lcfls1N  35842  fz1eqin  36350  issdrg  36786  sdrgacs  36790  isdomn3  36801  rp-isfinite6  36883  snhesn  37100  iotasbc2  37643  eelT00  37951  eelTTT  37952  eelT11  37953  eelT12  37955  eelTT1  37956  eelT01  37957  eel0T1  37958  uun132  38033  uun132p1  38034  un2122  38038  uunTT1  38041  uunTT1p1  38042  uunTT1p2  38043  uunT11  38044  uunT11p1  38045  uunT11p2  38046  uunT12  38047  uunT12p1  38048  uunT12p2  38049  uunT12p3  38050  uunT12p4  38051  uunT12p5  38052  uun111  38053  uun2221  38061  uun2221p1  38062  uun2221p2  38063  stoweidlem17  38910  stoweidlem34  38927  stoweidlem60  38953  ndmaovass  39935  ndmaovdistr  39936  reuccatpfxs1  40297  rexdifpr  40315  2elfz3nn0  40353  uspgredg2v  40451  nbgrel  40564  nb3grpr2  40611  isrusgr0  40766  rusgrprop0  40767  ewlkprop  40805  1wlksfval  40811  wlksfval  40812  wlkbProp  40817  1wlkeq  40838  wlkson  40864  wlkOnprop  40866  upgr2wlk  40876  upgrtrls  40909  upgristrl  40910  1wlksonproplem  40912  upgrwlkdvde  40943  isspthonpth-av  40955  spthonepeq-av  40958  uhgr1wlkspth  40961  usgr2wlkneq  40962  usgr2wlkspth  40965  usgr2pth  40970  crctcsh1wlkn0lem4  41016  wspthnp  41048  wwlknon  41053  wwlksnextwrd  41103  wwlksnextinj  41105  wspthsnwspthsnon  41122  umgr2adedgwlk  41152  umgr2adedgwlkon  41153  umgr2adedgwlkonALT  41154  umgr2adedgspth  41155  s3wwlks2on  41160  wpthswwlks2on  41164  usgr2wspthons3  41167  usgr2wspthon  41168  elwwlks2  41170  elwspths2spth  41171  rusgrnumwwlkl1  41172  isclwwlks  41188  clwwlkbp  41191  clwwlknp  41195  isclwwlksnx  41197  clwlkclwwlklem3  41210  clwwlksn2  41217  clwlksfclwwlk  41269  0pth-av  41293  1to3vfriswmgr  41450  3cyclfrgr  41458  av-numclwwlkovgel  41519  av-numclwwlk6  41544  isrng  41666  2zrngnmrid  41740  lindslinindsimp2lem5  42045  elpg  42256  alimp-no-surprise  42336