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  27303  scutbday  27306  addscut2  27465  mulscut2  27592  ax5seg  28227  eengtrkg  28275  uspgredg2v  28512  nb3grpr2  28671  isrusgr0  28854  rusgrprop0  28855  ewlkprop  28891  wksfval  28897  wlkeq  28922  wlkson  28944  wlkonprop  28946  upgr2wlk  28956  upgrtrls  28989  upgristrl  28990  wksonproplem  28992  wksonproplemOLD  28993  pthsfval  29009  ispth  29011  isspthonpth  29037  uhgrwkspth  29043  usgr2wlkspth  29047  crctcshwlkn0lem4  29098  wspthnp  29135  wwlknon  29142  wwlksnextwrd  29182  wwlksnextinj  29184  wspthsnwspthsnon  29201  umgr2adedgwlk  29230  umgr2adedgwlkon  29231  umgr2adedgwlkonALT  29232  umgr2adedgspth  29233  s3wwlks2on  29241  wpthswwlks2on  29246  usgr2wspthons3  29249  usgr2wspthon  29250  elwwlks2  29251  elwspths2spth  29252  rusgrnumwwlkl1  29253  rusgrnumwwlkslem  29254  isclwwlk  29268  clwwlkbp  29269  clwlkclwwlklem3  29285  isclwwlknx  29320  clwwlknp  29321  clwwlkn1  29325  clwwlkn2  29328  clwwlkwwlksb  29338  clwwlknonel  29379  0pth  29409  frcond4  29554  1to3vfriswmgr  29564  3cyclfrgr  29572  frgrwopreglem5  29605  2clwwlk2clwwlk  29634  numclwlk1lem1  29653  numclwwlk6  29674  ajval  30145  issh  30492  dmadjss  31171  adjeu  31173  adjval  31174  isst  31497  ishst  31498  xrdifh  32022  nndiffz1  32028  xdivpnfrp  32130  isomnd  32250  isslmd  32378  isprmidl  32587  isprmidlc  32597  ismxidl  32609  ressply1mon1p  32688  isrrext  33011  ismntop  33037  isros  33197  issros  33204  issibf  33363  eulerpartleme  33393  eulerpartlemt0  33399  probun  33449  bnj250  33743  bnj255  33747  bnj345  33756  bnj945  33815  bnj1209  33838  bnj1275  33855  bnj543  33935  bnj571  33948  bnj607  33958  bnj882  33968  bnj983  33993  bnj996  33998  bnj1006  34002  bnj1033  34011  bnj1097  34023  bnj1110  34024  bnj1145  34035  bnj1174  34045  bnj1189  34051  bnj1450  34092  bnj1514  34105  cusgr3cyclex  34158  erdszelem1  34213  cvmsval  34288  cvmliftiota  34323  snmlval  34353  lediv2aALT  34693  elwlim  34826  brtxp2  34884  brpprod3a  34889  brcart  34935  brsuccf  34944  broutsideof3  35129  gg-cnfldfunALT  35229  ivthALT  35268  df3nandALT2  35333  andnand1  35334  topdifinffinlem  36276  relowlssretop  36292  rdgeqoa  36299  unccur  36519  fin2solem  36522  poimirlem3  36539  poimirlem4  36540  poimirlem26  36562  poimirlem27  36563  poimirlem32  36568  itg2gt0cn  36591  iblabsnclem  36599  areacirc  36629  neificl  36669  ablo4pnp  36796  isrngohom  36881  isidl  36930  ispridl  36950  pridlidl  36951  ismaxidl  36956  maxidlidl  36957  isfldidl2  36985  isdmn3  36990  triantru3  37142  moantr  37281  brxrn2  37293  dfxrn2  37294  ecxrn  37305  disjressuc2  37306  inxpxrn  37313  rnxrn  37316  islshp  37897  isopos  38098  cvrfval  38186  cvrval  38187  isatl  38217  isat3  38225  islpln5  38454  4atlem11  38528  dalem20  38612  lhpexle3  38931  lhpex2leN  38932  isltrn2N  39039  diclspsn  40113  lcfls1lem  40453  lcfls1N  40454  uzindd  40890  flt4lem5e  41446  3cubes  41476  fz1eqin  41555  isdomn3  41994  dflim6  42062  dflim7  42071  nnoeomeqom  42110  cantnfub2  42120  fzunt  42254  fzuntd  42255  fzunt1d  42256  fzuntgd  42257  rp-isfinite6  42317  snhesn  42585  ismnuprim  43101  ismnushort  43108  iotasbc2  43227  eelT00  43514  eelTTT  43515  eelT11  43516  eelT12  43518  eelTT1  43519  eelT01  43520  eel0T1  43521  uun132  43594  uun132p1  43595  un2122  43599  uunTT1  43602  uunTT1p1  43603  uunTT1p2  43604  uunT11  43605  uunT11p1  43606  uunT11p2  43607  uunT12  43608  uunT12p1  43609  uunT12p2  43610  uunT12p3  43611  uunT12p4  43612  uunT12p5  43613  uun111  43614  uun2221  43622  uun2221p1  43623  uun2221p2  43624  stoweidlem17  44781  stoweidlem34  44798  stoweidlem60  44824  ndmaovass  45962  ndmaovdistr  45963  4an21  46026  2elfz3nn0  46072  prproropf1o  46223  fpprel  46444  upwlksfval  46561  isupwlkg  46563  upwlkbprop  46564  isrng  46698  issubrng  46774  ecqusadd  46816  ecqusaddcl  46817  qusmulrng  46818  rngqiprngghmlem3  46822  rngqiprnglinlem3  46826  rngqiprnglin  46835  2zrngnmrid  46896  lindslinindsimp2lem5  47191  i0oii  47600  io1ii  47601  sepnsepolem1  47602  iscnrm3lem3  47616  isthincd2  47706  functhinc  47713  elpg  47807  alimp-no-surprise  47876