Theorem 3anass 1096

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 1090	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 470	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3anan12  1097  3ancoma  1099  anandi3  1103  3biant1d  1479  an33rean  1484  an33reanOLD  1485  cad1  1619  3exdistr  1965  ceqsex2  3530  ceqsex2v  3531  ceqsex3v  3532  ceqsex4v  3533  ceqsex6v  3534  ceqsex8v  3535  2reu5lem1  3752  2reu5lem2  3753  2reu5lem3  3754  eldifpr  4661  rexdifpr  4662  trel3  5276  2rbropap  5567  ordelord  6387  dflim2  6422  dff1o4  6842  foco2  7109  brfvopab  7466  eloprabga  7516  ndmovass  7595  ndmovdistr  7596  dflim3  7836  dflim4  7837  frxp2  8130  mpoxopovel  8205  dfsmo2  8347  dfrecs3  8372  dfrecs3OLD  8373  oeeui  8602  naddasslem2  8694  ecopovtrn  8814  elixp2  8895  elixp  8898  mptelixpg  8929  dif1en  9160  dif1enOLD  9162  ssfi  9173  sbthfilem  9201  eqinf  9479  zorn2lem7  10497  grothprim  10829  grothtsk  10830  divmulasscom  11896  muldivdir  11907  divmuldiv  11914  sup3  12171  dfnn3  12226  prime  12643  eluz2  12828  raluz2  12881  elixx1  13333  elixx3g  13337  elioo2  13365  elioo5  13381  elicc4  13391  iccneg  13449  icoshft  13450  difreicc  13461  elfz1  13489  elfz  13490  elfz2  13491  elfzm11  13572  elfz2nn0  13592  elfzo2  13635  elfzo3  13649  lbfzo0  13672  fzind2  13750  zmodid2  13864  hashgt23el  14384  swrdnd2  14605  swrdnd0  14607  swrdccatin1  14675  swrdccat  14685  repswswrd  14734  swrdco  14788  2swrd2eqwrdeq  14904  rediv  15078  imdiv  15085  cosmul  16116  bitsval  16365  bitsmod  16377  bitscmp  16379  smueqlem  16431  dfgcd2  16488  lcmneg  16540  lcmftp  16573  coprmgcdb  16586  divgcdcoprmex  16603  cncongr1  16604  cncongr2  16605  difsqpwdvds  16820  oddprmdvds  16836  elgz  16864  xpsfrnel  17508  xpsfrnel2  17510  ismre  17534  mreexexlem4d  17591  iscatd2  17625  isssc  17767  eldmcoa  18015  isdrs  18254  isipodrs  18490  mgmsscl  18566  ismhm  18673  mhmpropd  18678  issubm  18684  issubmndb  18686  submacs  18708  issubg  19006  eqglact  19059  eqgid  19060  pgrpsubgsymgbi  19276  isslw  19476  efgsdm  19598  mulgmhm  19695  mulgghm  19696  dmdprd  19868  dprdw  19880  subgdmdprd  19904  dmdprdpr  19919  issrg  20011  srglmhm  20044  srgrmhm  20045  isring  20060  ringlghm  20124  dfrhm2  20253  issubrg3  20347  issdrg  20404  sdrgacs  20417  islmod  20475  lsspropd  20628  islmhm  20638  islbs  20687  lbspropd  20710  cnfldfunALT  20957  isphl  21181  elocv  21221  isobs  21275  mat1dimscm  21977  scmatghm  22035  scmatmhm  22036  ma1repvcl  22072  smadiadetr  22177  mat2pmatghm  22232  mat2pmatmul  22233  decpmatmulsumfsupp  22275  pm2mpghm  22318  pm2mpmhmlem1  22320  neindisj  22621  lmbrf  22764  hauscmplem  22910  llyi  22978  subislly  22985  islocfin  23021  uptx  23129  txcn  23130  qtopeu  23220  elmptrab  23331  isfbas  23333  trfil2  23391  flimcls  23489  cnextcn  23571  xmetec  23940  ngppropd  24146  ngpocelbl  24221  bl2ioo  24308  xrtgioo  24322  om1elbas  24548  elpi1  24561  isclm  24580  isclmp  24613  isncvsngp  24666  iscph  24687  tcphcph  24754  lmmbr2  24776  lmmbrf  24779  iscau2  24794  caussi  24814  lmclim  24820  bcthlem1  24841  srabn  24877  ishl2  24887  evthicc2  24977  ovolfioo  24984  ovolficc  24985  iblcnlem1  25305  iblrelem  25308  iblre  25311  iblcn  25316  isuc1p  25658  ismon1p  25660  ellogrn  26068  logreclem  26267  atandm  26381  atandm2  26382  atandm3  26383  atans2  26436  dmarea  26462  dchrelbas4  26746  lgsmodeq  26845  lgsmulsqcoprm  26846  nocvxminlem  27279  scutcut  27302  scutbday  27305  addscut2  27463  mulscut2  27589  ax5seg  28196  eengtrkg  28244  uspgredg2v  28481  nb3grpr2  28640  isrusgr0  28823  rusgrprop0  28824  ewlkprop  28860  wksfval  28866  wlkeq  28891  wlkson  28913  wlkonprop  28915  upgr2wlk  28925  upgrtrls  28958  upgristrl  28959  wksonproplem  28961  wksonproplemOLD  28962  pthsfval  28978  ispth  28980  isspthonpth  29006  uhgrwkspth  29012  usgr2wlkspth  29016  crctcshwlkn0lem4  29067  wspthnp  29104  wwlknon  29111  wwlksnextwrd  29151  wwlksnextinj  29153  wspthsnwspthsnon  29170  umgr2adedgwlk  29199  umgr2adedgwlkon  29200  umgr2adedgwlkonALT  29201  umgr2adedgspth  29202  s3wwlks2on  29210  wpthswwlks2on  29215  usgr2wspthons3  29218  usgr2wspthon  29219  elwwlks2  29220  elwspths2spth  29221  rusgrnumwwlkl1  29222  rusgrnumwwlkslem  29223  isclwwlk  29237  clwwlkbp  29238  clwlkclwwlklem3  29254  isclwwlknx  29289  clwwlknp  29290  clwwlkn1  29294  clwwlkn2  29297  clwwlkwwlksb  29307  clwwlknonel  29348  0pth  29378  frcond4  29523  1to3vfriswmgr  29533  3cyclfrgr  29541  frgrwopreglem5  29574  2clwwlk2clwwlk  29603  numclwlk1lem1  29622  numclwwlk6  29643  ajval  30114  issh  30461  dmadjss  31140  adjeu  31142  adjval  31143  isst  31466  ishst  31467  xrdifh  31991  nndiffz1  31997  xdivpnfrp  32099  isomnd  32219  isslmd  32347  isprmidl  32556  isprmidlc  32566  ismxidl  32578  ressply1mon1p  32657  isrrext  32980  ismntop  33006  isros  33166  issros  33173  issibf  33332  eulerpartleme  33362  eulerpartlemt0  33368  probun  33418  bnj250  33712  bnj255  33716  bnj345  33725  bnj945  33784  bnj1209  33807  bnj1275  33824  bnj543  33904  bnj571  33917  bnj607  33927  bnj882  33937  bnj983  33962  bnj996  33967  bnj1006  33971  bnj1033  33980  bnj1097  33992  bnj1110  33993  bnj1145  34004  bnj1174  34014  bnj1189  34020  bnj1450  34061  bnj1514  34074  cusgr3cyclex  34127  erdszelem1  34182  cvmsval  34257  cvmliftiota  34292  snmlval  34322  lediv2aALT  34662  elwlim  34795  brtxp2  34853  brpprod3a  34858  brcart  34904  brsuccf  34913  broutsideof3  35098  ivthALT  35220  df3nandALT2  35285  andnand1  35286  topdifinffinlem  36228  relowlssretop  36244  rdgeqoa  36251  unccur  36471  fin2solem  36474  poimirlem3  36491  poimirlem4  36492  poimirlem26  36514  poimirlem27  36515  poimirlem32  36520  itg2gt0cn  36543  iblabsnclem  36551  areacirc  36581  neificl  36621  ablo4pnp  36748  isrngohom  36833  isidl  36882  ispridl  36902  pridlidl  36903  ismaxidl  36908  maxidlidl  36909  isfldidl2  36937  isdmn3  36942  triantru3  37094  moantr  37233  brxrn2  37245  dfxrn2  37246  ecxrn  37257  disjressuc2  37258  inxpxrn  37265  rnxrn  37268  islshp  37849  isopos  38050  cvrfval  38138  cvrval  38139  isatl  38169  isat3  38177  islpln5  38406  4atlem11  38480  dalem20  38564  lhpexle3  38883  lhpex2leN  38884  isltrn2N  38991  diclspsn  40065  lcfls1lem  40405  lcfls1N  40406  uzindd  40842  flt4lem5e  41398  3cubes  41428  fz1eqin  41507  isdomn3  41946  dflim6  42014  dflim7  42023  nnoeomeqom  42062  cantnfub2  42072  fzunt  42206  fzuntd  42207  fzunt1d  42208  fzuntgd  42209  rp-isfinite6  42269  snhesn  42537  ismnuprim  43053  ismnushort  43060  iotasbc2  43179  eelT00  43466  eelTTT  43467  eelT11  43468  eelT12  43470  eelTT1  43471  eelT01  43472  eel0T1  43473  uun132  43546  uun132p1  43547  un2122  43551  uunTT1  43554  uunTT1p1  43555  uunTT1p2  43556  uunT11  43557  uunT11p1  43558  uunT11p2  43559  uunT12  43560  uunT12p1  43561  uunT12p2  43562  uunT12p3  43563  uunT12p4  43564  uunT12p5  43565  uun111  43566  uun2221  43574  uun2221p1  43575  uun2221p2  43576  stoweidlem17  44733  stoweidlem34  44750  stoweidlem60  44776  ndmaovass  45914  ndmaovdistr  45915  4an21  45978  2elfz3nn0  46024  prproropf1o  46175  fpprel  46396  upwlksfval  46513  isupwlkg  46515  upwlkbprop  46516  isrng  46650  issubrng  46726  ecqusadd  46768  ecqusaddcl  46769  qusmulrng  46770  rngqiprngghmlem3  46774  rngqiprnglinlem3  46778  rngqiprnglin  46787  2zrngnmrid  46848  lindslinindsimp2lem5  47143  i0oii  47552  io1ii  47553  sepnsepolem1  47554  iscnrm3lem3  47568  isthincd2  47658  functhinc  47665  elpg  47759  alimp-no-surprise  47828