Theorem 3anass 1094

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anan12  1095  3ancoma  1097  anandi3  1101  4anpull2  1362  3biant1d  1480  an33rean  1485  cad1  1617  3exdistr  1960  ceqsex2  3490  ceqsex2v  3491  ceqsex3v  3492  ceqsex4v  3493  ceqsex6v  3494  ceqsex8v  3495  2reu5lem1  3715  2reu5lem2  3716  2reu5lem3  3717  eldifpr  4610  rexdifpr  4611  trel3  5208  2rbropap  5507  ordelord  6329  dflim2  6365  dff1o4  6772  foco2  7043  brfvopab  7406  eloprabga  7458  ndmovass  7537  ndmovdistr  7538  dflim3  7780  dflim4  7781  frxp2  8077  mpoxopovel  8153  dfsmo2  8270  dfrecs3  8295  oeeui  8520  naddasslem2  8613  ecopovtrn  8747  elixp2  8828  elixp  8831  mptelixpg  8862  dif1en  9075  ssfi  9087  sbthfilem  9112  eqinf  9375  zorn2lem7  10396  grothprim  10728  grothtsk  10729  divmulasscom  11803  muldivdir  11817  divmuldiv  11824  sup3  12082  dfnn3  12142  prime  12557  eluz2  12741  raluz2  12798  elixx1  13257  elixx3g  13261  elioo2  13289  elioo5  13306  elicc4  13316  iccneg  13375  icoshft  13376  difreicc  13387  elfz1  13415  elfz  13416  elfz2  13417  elfzm11  13498  elfz2nn0  13521  elfzo2  13565  elfzo3  13579  lbfzo0  13602  fzo1lb  13616  1elfzo1  13617  fzind2  13688  zmodid2  13803  hashgt23el  14331  swrdnd2  14562  swrdnd0  14564  swrdccatin1  14631  swrdccat  14641  repswswrd  14690  swrdco  14744  2swrd2eqwrdeq  14860  rediv  15038  imdiv  15045  cosmul  16082  bitsval  16335  bitsmod  16347  bitscmp  16349  smueqlem  16401  dfgcd2  16457  lcmneg  16514  lcmftp  16547  coprmgcdb  16560  divgcdcoprmex  16577  cncongr1  16578  cncongr2  16579  difsqpwdvds  16799  oddprmdvds  16815  elgz  16843  xpsfrnel  17466  xpsfrnel2  17468  ismre  17492  mreexexlem4d  17553  iscatd2  17587  isssc  17727  eldmcoa  17972  isdrs  18207  isipodrs  18443  mgmsscl  18519  ismhm  18659  mhmpropd  18666  issubm  18677  issubmndb  18679  submacs  18701  issubg  19005  eqglact  19058  eqgid  19059  ecqusaddd  19071  ecqusaddcl  19072  pgrpsubgsymgbi  19287  isslw  19487  efgsdm  19609  mulgmhm  19706  mulgghm  19707  dmdprd  19879  dprdw  19891  subgdmdprd  19915  dmdprdpr  19930  isomnd  20002  isrng  20039  issrg  20073  srglmhm  20106  srgrmhm  20107  isring  20122  ringlghm  20197  dfrhm2  20359  issubrng  20432  issubrg3  20485  isdomn3  20600  issdrg  20673  sdrgacs  20686  islmod  20767  lsspropd  20921  islmhm  20931  islbs  20980  lbspropd  21003  qusmulrng  21189  rngqiprngghmlem3  21196  rngqiprnglinlem3  21200  rngqiprnglin  21209  cnfldfunALT  21276  cnfldfunALTOLD  21289  isphl  21535  elocv  21575  isobs  21627  mat1dimscm  22360  scmatghm  22418  scmatmhm  22419  ma1repvcl  22455  smadiadetr  22560  mat2pmatghm  22615  mat2pmatmul  22616  decpmatmulsumfsupp  22658  pm2mpghm  22701  pm2mpmhmlem1  22703  neindisj  23002  lmbrf  23145  hauscmplem  23291  llyi  23359  subislly  23366  islocfin  23402  uptx  23510  txcn  23511  qtopeu  23601  elmptrab  23712  isfbas  23714  trfil2  23772  flimcls  23870  cnextcn  23952  xmetec  24320  ngppropd  24523  ngpocelbl  24590  bl2ioo  24678  xrtgioo  24693  om1elbas  24930  elpi1  24943  isclm  24962  isclmp  24995  isncvsngp  25047  iscph  25068  tcphcph  25135  lmmbr2  25157  lmmbrf  25160  iscau2  25175  caussi  25195  lmclim  25201  bcthlem1  25222  srabn  25258  ishl2  25268  evthicc2  25359  ovolfioo  25366  ovolficc  25367  iblcnlem1  25687  iblrelem  25690  iblre  25693  iblcn  25698  isuc1p  26044  ismon1p  26046  ellogrn  26466  logreclem  26670  atandm  26784  atandm2  26785  atandm3  26786  atans2  26839  dmarea  26865  dchrelbas4  27152  lgsmodeq  27251  lgsmulsqcoprm  27252  nocvxminlem  27688  scutcut  27713  scutbday  27716  addscut2  27893  mulscut2  28043  ax5seg  28887  eengtrkg  28935  uspgredg2v  29173  nb3grpr2  29332  isrusgr0  29516  rusgrprop0  29517  ewlkprop  29553  wksfval  29559  wlkeq  29583  wlkson  29604  wlkonprop  29606  upgr2wlk  29616  upgrtrls  29649  upgristrl  29650  wksonproplem  29652  pthsfval  29668  ispth  29670  dfpth2  29678  isspthonpth  29698  uhgrwkspth  29704  usgr2wlkspth  29708  crctcshwlkn0lem4  29762  wspthnp  29799  wwlknon  29806  wwlksnextwrd  29846  wwlksnextinj  29848  wspthsnwspthsnon  29865  umgr2adedgwlk  29894  umgr2adedgwlkon  29895  umgr2adedgwlkonALT  29896  umgr2adedgspth  29897  s3wwlks2on  29905  wpthswwlks2on  29910  usgr2wspthons3  29913  usgr2wspthon  29914  elwwlks2  29915  elwspths2spth  29916  rusgrnumwwlkl1  29917  rusgrnumwwlkslem  29918  isclwwlk  29932  clwwlkbp  29933  clwlkclwwlklem3  29949  isclwwlknx  29984  clwwlknp  29985  clwwlkn1  29989  clwwlkn2  29992  clwwlkwwlksb  30002  clwwlknonel  30043  0pth  30073  frcond4  30218  1to3vfriswmgr  30228  3cyclfrgr  30236  frgrwopreglem5  30269  2clwwlk2clwwlk  30298  numclwlk1lem1  30317  numclwwlk6  30338  ajval  30809  issh  31156  dmadjss  31835  adjeu  31837  adjval  31838  isst  32161  ishst  32162  xrdifh  32732  nndiffz1  32738  xdivpnfrp  32882  isslmd  33153  isprmidl  33384  isprmidlc  33393  ismxidl  33408  ressply1mon1p  33512  isrrext  33983  ismntop  34009  isros  34151  issros  34158  issibf  34317  eulerpartleme  34347  eulerpartlemt0  34353  probun  34403  bnj250  34684  bnj255  34688  bnj345  34697  bnj945  34756  bnj1209  34779  bnj1275  34796  bnj543  34876  bnj571  34889  bnj607  34899  bnj882  34909  bnj983  34934  bnj996  34939  bnj1006  34943  bnj1033  34952  bnj1097  34964  bnj1110  34965  bnj1145  34976  bnj1174  34986  bnj1189  34992  bnj1450  35033  bnj1514  35046  wevgblacfn  35102  cusgr3cyclex  35129  erdszelem1  35184  cvmsval  35259  cvmliftiota  35294  snmlval  35324  lediv2aALT  35670  elwlim  35817  brtxp2  35875  brpprod3a  35880  brcart  35926  brsuccf  35935  broutsideof3  36120  ivthALT  36329  df3nandALT2  36394  andnand1  36395  topdifinffinlem  37341  relowlssretop  37357  rdgeqoa  37364  unccur  37603  fin2solem  37606  poimirlem3  37623  poimirlem4  37624  poimirlem26  37646  poimirlem27  37647  poimirlem32  37652  itg2gt0cn  37675  iblabsnclem  37683  areacirc  37713  neificl  37753  ablo4pnp  37880  isrngohom  37965  isidl  38014  ispridl  38034  pridlidl  38035  ismaxidl  38040  maxidlidl  38041  isfldidl2  38069  isdmn3  38074  triantru3  38224  moantr  38352  brxrn2  38363  dfxrn2  38364  ecxrn  38379  disjressuc2  38380  inxpxrn  38387  rnxrn  38390  dmqsblocks  38851  islshp  38978  isopos  39179  cvrfval  39267  cvrval  39268  isatl  39298  isat3  39306  islpln5  39534  4atlem11  39608  dalem20  39692  lhpexle3  40011  lhpex2leN  40012  isltrn2N  40119  diclspsn  41193  lcfls1lem  41533  lcfls1N  41534  uzindd  41970  isprimroot  42086  flt4lem5e  42649  3cubes  42683  fz1eqin  42762  dflim6  43257  dflim7  43266  nnoeomeqom  43305  cantnfub2  43315  fzunt  43448  fzuntd  43449  fzunt1d  43450  fzuntgd  43451  rp-isfinite6  43511  snhesn  43779  ismnuprim  44287  ismnushort  44294  iotasbc2  44413  eelT00  44698  eelTTT  44699  eelT11  44700  eelT12  44702  eelTT1  44703  eelT01  44704  eel0T1  44705  uun132  44778  uun132p1  44779  un2122  44783  uunTT1  44786  uunTT1p1  44787  uunTT1p2  44788  uunT11  44789  uunT11p1  44790  uunT11p2  44791  uunT12  44792  uunT12p1  44793  uunT12p2  44794  uunT12p3  44795  uunT12p4  44796  uunT12p5  44797  uun111  44798  uun2221  44806  uun2221p1  44807  uun2221p2  44808  stoweidlem17  46018  stoweidlem34  46035  stoweidlem60  46061  ndmaovass  47210  ndmaovdistr  47211  4an21  47274  2elfz3nn0  47320  difltmodne  47346  prproropf1o  47511  fpprel  47732  clnbgredg  47844  dfvopnbgr2  47857  dfclnbgr6  47860  dfnbgr6  47861  dfsclnbgr6  47862  uhgrimprop  47896  isuspgrimlem  47899  clnbgrgrim  47938  isgrtri  47947  isubgr3stgrlem4  47973  isubgr3stgrlem7  47976  upwlksfval  48139  isupwlkg  48141  upwlkbprop  48142  2zrngnmrid  48260  lindslinindsimp2lem5  48467  i0oii  48924  io1ii  48925  sepnsepolem1  48926  isthincd2  49442  functhinc  49453  elpg  49719  alimp-no-surprise  49786