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  3514  ceqsex2v  3515  ceqsex3v  3516  ceqsex4v  3517  ceqsex6v  3518  ceqsex8v  3519  2reu5lem1  3738  2reu5lem2  3739  2reu5lem3  3740  eldifpr  4634  rexdifpr  4635  trel3  5239  2rbropap  5541  ordelord  6374  dflim2  6410  dff1o4  6825  foco2  7098  brfvopab  7462  eloprabga  7514  ndmovass  7593  ndmovdistr  7594  dflim3  7840  dflim4  7841  frxp2  8141  mpoxopovel  8217  dfsmo2  8359  dfrecs3  8384  dfrecs3OLD  8385  oeeui  8612  naddasslem2  8705  ecopovtrn  8832  elixp2  8913  elixp  8916  mptelixpg  8947  dif1en  9172  dif1enOLD  9174  ssfi  9185  sbthfilem  9210  eqinf  9495  zorn2lem7  10514  grothprim  10846  grothtsk  10847  divmulasscom  11918  muldivdir  11932  divmuldiv  11939  sup3  12197  dfnn3  12252  prime  12672  eluz2  12856  raluz2  12911  elixx1  13369  elixx3g  13373  elioo2  13401  elioo5  13418  elicc4  13428  iccneg  13487  icoshft  13488  difreicc  13499  elfz1  13527  elfz  13528  elfz2  13529  elfzm11  13610  elfz2nn0  13633  elfzo2  13677  elfzo3  13691  lbfzo0  13714  fzo1lb  13728  fzind2  13799  zmodid2  13914  hashgt23el  14440  swrdnd2  14671  swrdnd0  14673  swrdccatin1  14741  swrdccat  14751  repswswrd  14800  swrdco  14854  2swrd2eqwrdeq  14970  rediv  15148  imdiv  15155  cosmul  16189  bitsval  16441  bitsmod  16453  bitscmp  16455  smueqlem  16507  dfgcd2  16563  lcmneg  16620  lcmftp  16653  coprmgcdb  16666  divgcdcoprmex  16683  cncongr1  16684  cncongr2  16685  difsqpwdvds  16905  oddprmdvds  16921  elgz  16949  xpsfrnel  17574  xpsfrnel2  17576  ismre  17600  mreexexlem4d  17657  iscatd2  17691  isssc  17831  eldmcoa  18076  isdrs  18311  isipodrs  18545  mgmsscl  18621  ismhm  18761  mhmpropd  18768  issubm  18779  issubmndb  18781  submacs  18803  issubg  19107  eqglact  19160  eqgid  19161  ecqusaddd  19173  ecqusaddcl  19174  pgrpsubgsymgbi  19387  isslw  19587  efgsdm  19709  mulgmhm  19806  mulgghm  19807  dmdprd  19979  dprdw  19991  subgdmdprd  20015  dmdprdpr  20030  isrng  20112  issrg  20146  srglmhm  20179  srgrmhm  20180  isring  20195  ringlghm  20270  dfrhm2  20432  issubrng  20505  issubrg3  20558  isdomn3  20673  issdrg  20746  sdrgacs  20759  islmod  20819  lsspropd  20973  islmhm  20983  islbs  21032  lbspropd  21055  qusmulrng  21241  rngqiprngghmlem3  21248  rngqiprnglinlem3  21252  rngqiprnglin  21261  cnfldfunALT  21328  cnfldfunALTOLD  21341  isphl  21586  elocv  21626  isobs  21678  mat1dimscm  22411  scmatghm  22469  scmatmhm  22470  ma1repvcl  22506  smadiadetr  22611  mat2pmatghm  22666  mat2pmatmul  22667  decpmatmulsumfsupp  22709  pm2mpghm  22752  pm2mpmhmlem1  22754  neindisj  23053  lmbrf  23196  hauscmplem  23342  llyi  23410  subislly  23417  islocfin  23453  uptx  23561  txcn  23562  qtopeu  23652  elmptrab  23763  isfbas  23765  trfil2  23823  flimcls  23921  cnextcn  24003  xmetec  24371  ngppropd  24574  ngpocelbl  24641  bl2ioo  24729  xrtgioo  24744  om1elbas  24981  elpi1  24994  isclm  25013  isclmp  25046  isncvsngp  25099  iscph  25120  tcphcph  25187  lmmbr2  25209  lmmbrf  25212  iscau2  25227  caussi  25247  lmclim  25253  bcthlem1  25274  srabn  25310  ishl2  25320  evthicc2  25411  ovolfioo  25418  ovolficc  25419  iblcnlem1  25739  iblrelem  25742  iblre  25745  iblcn  25750  isuc1p  26096  ismon1p  26098  ellogrn  26518  logreclem  26722  atandm  26836  atandm2  26837  atandm3  26838  atans2  26891  dmarea  26917  dchrelbas4  27204  lgsmodeq  27303  lgsmulsqcoprm  27304  nocvxminlem  27739  scutcut  27763  scutbday  27766  addscut2  27929  mulscut2  28076  ax5seg  28863  eengtrkg  28911  uspgredg2v  29149  nb3grpr2  29308  isrusgr0  29492  rusgrprop0  29493  ewlkprop  29529  wksfval  29535  wlkeq  29560  wlkson  29582  wlkonprop  29584  upgr2wlk  29594  upgrtrls  29627  upgristrl  29628  wksonproplem  29630  wksonproplemOLD  29631  pthsfval  29647  ispth  29649  dfpth2  29657  isspthonpth  29677  uhgrwkspth  29683  usgr2wlkspth  29687  crctcshwlkn0lem4  29741  wspthnp  29778  wwlknon  29785  wwlksnextwrd  29825  wwlksnextinj  29827  wspthsnwspthsnon  29844  umgr2adedgwlk  29873  umgr2adedgwlkon  29874  umgr2adedgwlkonALT  29875  umgr2adedgspth  29876  s3wwlks2on  29884  wpthswwlks2on  29889  usgr2wspthons3  29892  usgr2wspthon  29893  elwwlks2  29894  elwspths2spth  29895  rusgrnumwwlkl1  29896  rusgrnumwwlkslem  29897  isclwwlk  29911  clwwlkbp  29912  clwlkclwwlklem3  29928  isclwwlknx  29963  clwwlknp  29964  clwwlkn1  29968  clwwlkn2  29971  clwwlkwwlksb  29981  clwwlknonel  30022  0pth  30052  frcond4  30197  1to3vfriswmgr  30207  3cyclfrgr  30215  frgrwopreglem5  30248  2clwwlk2clwwlk  30277  numclwlk1lem1  30296  numclwwlk6  30317  ajval  30788  issh  31135  dmadjss  31814  adjeu  31816  adjval  31817  isst  32140  ishst  32141  xrdifh  32703  nndiffz1  32709  xdivpnfrp  32853  isomnd  33015  isslmd  33145  isprmidl  33399  isprmidlc  33408  ismxidl  33423  ressply1mon1p  33527  isrrext  33977  ismntop  34003  isros  34145  issros  34152  issibf  34311  eulerpartleme  34341  eulerpartlemt0  34347  probun  34397  bnj250  34678  bnj255  34682  bnj345  34691  bnj945  34750  bnj1209  34773  bnj1275  34790  bnj543  34870  bnj571  34883  bnj607  34893  bnj882  34903  bnj983  34928  bnj996  34933  bnj1006  34937  bnj1033  34946  bnj1097  34958  bnj1110  34959  bnj1145  34970  bnj1174  34980  bnj1189  34986  bnj1450  35027  bnj1514  35040  wevgblacfn  35077  cusgr3cyclex  35104  erdszelem1  35159  cvmsval  35234  cvmliftiota  35269  snmlval  35299  lediv2aALT  35645  elwlim  35787  brtxp2  35845  brpprod3a  35850  brcart  35896  brsuccf  35905  broutsideof3  36090  ivthALT  36299  df3nandALT2  36364  andnand1  36365  topdifinffinlem  37311  relowlssretop  37327  rdgeqoa  37334  unccur  37573  fin2solem  37576  poimirlem3  37593  poimirlem4  37594  poimirlem26  37616  poimirlem27  37617  poimirlem32  37622  itg2gt0cn  37645  iblabsnclem  37653  areacirc  37683  neificl  37723  ablo4pnp  37850  isrngohom  37935  isidl  37984  ispridl  38004  pridlidl  38005  ismaxidl  38010  maxidlidl  38011  isfldidl2  38039  isdmn3  38044  triantru3  38194  moantr  38328  brxrn2  38339  dfxrn2  38340  ecxrn  38351  disjressuc2  38352  inxpxrn  38359  rnxrn  38362  islshp  38943  isopos  39144  cvrfval  39232  cvrval  39233  isatl  39263  isat3  39271  islpln5  39500  4atlem11  39574  dalem20  39658  lhpexle3  39977  lhpex2leN  39978  isltrn2N  40085  diclspsn  41159  lcfls1lem  41499  lcfls1N  41500  uzindd  41936  isprimroot  42052  flt4lem5e  42626  3cubes  42660  fz1eqin  42739  dflim6  43235  dflim7  43244  nnoeomeqom  43283  cantnfub2  43293  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  rp-isfinite6  43489  snhesn  43757  ismnuprim  44266  ismnushort  44273  iotasbc2  44392  eelT00  44677  eelTTT  44678  eelT11  44679  eelT12  44681  eelTT1  44682  eelT01  44683  eel0T1  44684  uun132  44757  uun132p1  44758  un2122  44762  uunTT1  44765  uunTT1p1  44766  uunTT1p2  44767  uunT11  44768  uunT11p1  44769  uunT11p2  44770  uunT12  44771  uunT12p1  44772  uunT12p2  44773  uunT12p3  44774  uunT12p4  44775  uunT12p5  44776  uun111  44777  uun2221  44785  uun2221p1  44786  uun2221p2  44787  stoweidlem17  45994  stoweidlem34  46011  stoweidlem60  46037  ndmaovass  47183  ndmaovdistr  47184  4an21  47247  2elfz3nn0  47293  difltmodne  47319  prproropf1o  47469  fpprel  47690  clnbgredg  47801  dfvopnbgr2  47814  dfclnbgr6  47817  dfnbgr6  47818  dfsclnbgr6  47819  uhgrimprop  47853  isuspgrimlem  47856  clnbgrgrim  47895  isgrtri  47903  isubgr3stgrlem4  47929  isubgr3stgrlem7  47932  upwlksfval  48058  isupwlkg  48060  upwlkbprop  48061  2zrngnmrid  48179  lindslinindsimp2lem5  48386  i0oii  48842  io1ii  48843  sepnsepolem1  48844  isthincd2  49271  functhinc  49282  elpg  49526  alimp-no-surprise  49593