Theorem 3anass 1109

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 1103	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 473	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anan12  1110  3ancoma  1113  anandi3  1117  4anpull2OLD  1381  3biant1d  1506  an33rean  1511  cad1  1644  3exdistr  1987  ceqsex2  3511  ceqsex2v  3512  ceqsex3v  3513  ceqsex4v  3514  ceqsex6v  3515  ceqsex8v  3516  2reu5lem1  3725  2reu5lem2  3726  2reu5lem3  3727  eldifpr  4627  rexdifpr  4628  trel3  5229  2rbropap  5550  ordelord  6383  dflim2  6420  dff1o4  6830  foco2  7105  brfvopab  7468  eloprabga  7520  ndmovass  7599  ndmovdistr  7600  dflim3  7843  dflim4  7844  frxp2  8140  mpoxopovel  8216  dfsmo2  8334  dfrecs3  8359  oeeui  8588  naddasslem2  8682  ecopovtrn  8818  elixp2  8899  elixp  8902  mptelixpg  8933  dif1en  9146  ssfi  9157  sbthfilem  9182  eqinf  9445  zorn2lem7  10486  grothprim  10819  grothtsk  10820  divmulasscom  11896  muldivdir  11907  divmuldiv  11915  sup3  12172  dfnn3  12247  prime  12677  eluz2  12868  raluz2  12921  elixx1  13381  elixx3g  13385  elioo2  13413  elioo5  13430  elicc4  13440  iccneg  13499  icoshft  13500  difreicc  13511  elfz1  13540  elfz  13541  elfz2  13542  elfzm11  13623  elfz2nn0  13646  elfzo2  13690  elfzo3  13705  lbfzo0  13728  fzo1lb  13742  1elfzo1  13743  fzind2  13817  zmodid2  13932  hashgt23el  14461  swrdnd2  14693  swrdnd0  14695  swrdccatin1  14762  swrdccat  14772  repswswrd  14821  swrdco  14874  2swrd2eqwrdeq  14990  rediv  15182  imdiv  15189  cosmul  16229  bitsval  16482  bitsmod  16494  bitscmp  16496  smueqlem  16548  dfgcd2  16604  lcmneg  16661  lcmftp  16694  coprmgcdb  16707  divgcdcoprmex  16724  cncongr1  16725  cncongr2  16726  difsqpwdvds  16947  oddprmdvds  16963  elgz  16991  xpsfrnel  17616  xpsfrnel2  17618  ismre  17642  mreexexlem4d  17703  iscatd2  17737  isssc  17877  eldmcoa  18122  isdrs  18357  isipodrs  18593  mgmsscl  18703  ismhm  18843  mhmpropd  18850  issubm  18861  issubmndb  18863  submacs  18886  issubg  19192  eqglact  19247  eqgid  19248  ecqusaddd  19263  ecqusaddcl  19264  pgrpsubgsymgbi  19478  isslw  19678  efgsdm  19800  mulgmhm  19897  mulgghm  19898  dmdprd  20070  dprdw  20082  subgdmdprd  20106  dmdprdpr  20121  isomnd  20193  isrng  20232  issrg  20270  srglmhm  20303  srgrmhm  20304  isring  20319  ringlghm  20395  dfrhm2  20556  issubrng  20632  issubrg3  20685  isdomn3  20799  issdrg  20869  sdrgacs  20882  islmod  20963  lsspropd  21116  islmhm  21126  islbs  21175  lbspropd  21198  qusmulrng  21393  rngqiprngghmlem3  21400  rngqiprnglinlem3  21404  rngqiprnglin  21413  isprmidl  21434  isprmidlc  21443  cnfldfunALT  21506  isphl  21747  elocv  21787  isobs  21839  mat1dimscm  22601  scmatghm  22659  scmatmhm  22660  ma1repvcl  22696  smadiadetr  22801  mat2pmatghm  22856  mat2pmatmul  22857  decpmatmulsumfsupp  22899  pm2mpghm  22942  pm2mpmhmlem1  22944  neindisj  23243  lmbrf  23386  hauscmplem  23532  llyi  23600  subislly  23607  islocfin  23643  uptx  23751  txcn  23752  qtopeu  23842  elmptrab  23953  isfbas  23955  trfil2  24013  flimcls  24111  cnextcn  24193  xmetec  24560  ngppropd  24763  ngpocelbl  24830  bl2ioo  24918  xrtgioo  24933  om1elbas  25160  elpi1  25173  isclm  25192  isclmp  25225  isncvsngp  25277  iscph  25298  tcphcph  25365  lmmbr2  25387  lmmbrf  25390  iscau2  25405  caussi  25425  lmclim  25431  bcthlem1  25452  srabn  25488  ishl2  25498  evthicc2  25588  ovolfioo  25595  ovolficc  25596  iblcnlem1  25916  iblrelem  25919  iblre  25922  iblcn  25927  isuc1p  26267  ismon1p  26269  ellogrn  26690  logreclem  26893  atandm  27007  atandm2  27008  atandm3  27009  atans2  27062  dmarea  27088  dchrelbas4  27373  lgsmodeq  27472  lgsmulsqcoprm  27473  nocvxminlem  27913  cutcuts  27940  cutbday  27943  addcuts2  28138  mulcut2  28292  ax5seg  29229  eengtrkg  29277  uspgredg2v  29515  nb3grpr2  29674  isrusgr0  29857  rusgrprop0  29858  ewlkprop  29894  wksfval  29900  wlkeq  29924  wlkson  29945  wlkonprop  29947  upgr2wlk  29957  upgrtrls  29990  upgristrl  29991  wksonproplem  29993  pthsfval  30009  ispth  30011  dfpth2  30019  isspthonpth  30039  uhgrwkspth  30045  usgr2wlkspth  30049  crctcshwlkn0lem4  30103  wspthnp  30140  wwlknon  30147  wwlksnextwrd  30187  wwlksnextinj  30189  wspthsnwspthsnon  30206  umgr2adedgwlk  30235  umgr2adedgwlkon  30236  umgr2adedgwlkonALT  30237  umgr2adedgspth  30238  s3wwlks2on  30246  sps3wwlks2on  30247  wpthswwlks2on  30254  usgr2wspthons3  30257  usgr2wspthon  30258  elwwlks2  30259  elwspths2spth  30260  rusgrnumwwlkl1  30261  rusgrnumwwlkslem  30262  isclwwlk  30276  clwwlkbp  30277  clwlkclwwlklem3  30293  isclwwlknx  30328  clwwlknp  30329  clwwlkn1  30333  clwwlkn2  30336  clwwlkwwlksb  30346  clwwlknonel  30387  0pth  30417  frcond4  30562  1to3vfriswmgr  30572  3cyclfrgr  30580  frgrwopreglem5  30613  2clwwlk2clwwlk  30642  numclwlk1lem1  30661  numclwwlk6  30682  ajval  31154  issh  31501  dmadjss  32180  adjeu  32182  adjval  32183  isst  32506  ishst  32507  xrdifh  33066  nndiffz1  33072  xdivpnfrp  33193  isslmd  33463  ismxidl  33690  ressply1mon1p  33803  isrrext  34335  ismntop  34361  isros  34503  issros  34510  issibf  34668  eulerpartleme  34698  eulerpartlemt0  34704  probun  34754  bnj250  35035  bnj255  35039  bnj345  35048  bnj945  35107  bnj1209  35129  bnj1275  35146  bnj543  35226  bnj571  35239  bnj607  35249  bnj882  35259  bnj983  35284  bnj996  35289  bnj1006  35293  bnj1033  35302  bnj1097  35314  bnj1110  35315  bnj1145  35326  bnj1174  35336  bnj1189  35342  bnj1450  35383  bnj1514  35396  axprALT2  35446  wevgblacfn  35528  cusgr3cyclex  35561  erdszelem1  35616  cvmsval  35691  cvmliftiota  35726  snmlval  35756  lediv2aALT  36102  elwlim  36246  brtxp2  36304  brpprod3a  36309  brcart  36355  lemsuccf  36364  broutsideof3  36551  ivthALT  36769  df3nandALT2  36834  andnand1  36835  topdifinffinlem  37916  relowlssretop  37932  rdgeqoa  37939  unccur  38177  fin2solem  38180  poimirlem3  38197  poimirlem4  38198  poimirlem26  38220  poimirlem27  38221  poimirlem32  38226  itg2gt0cn  38249  iblabsnclem  38257  areacirc  38287  neificl  38327  ablo4pnp  38454  isrngohom  38539  isidl  38588  ispridl  38608  pridlidl  38609  ismaxidl  38614  maxidlidl  38615  isfldidl2  38643  isdmn3  38648  triantru3  38810  moantr  38946  brxrn2  38958  dfxrn2  38959  ecxrn  38980  disjressuc2  38985  inxpxrn  38992  rnxrn  38995  dfsuccl4  39048  dmqsblocks  39541  islshp  39678  isopos  39879  cvrfval  39967  cvrval  39968  isatl  39998  isat3  40006  islpln5  40234  4atlem11  40308  dalem20  40392  lhpexle3  40711  lhpex2leN  40712  isltrn2N  40819  diclspsn  41893  lcfls1lem  42233  lcfls1N  42234  uzindd  42670  isprimroot  42785  flt4lem5e  43315  3cubes  43348  fz1eqin  43427  dflim6  43918  dflim7  43927  nnoeomeqom  43966  cantnfub2  43976  fzunt  44108  fzuntd  44109  fzunt1d  44110  fzuntgd  44111  rp-isfinite6  44171  snhesn  44439  ismnuprim  44931  ismnushort  44938  iotasbc2  45057  eelT00  45340  eelTTT  45341  eelT11  45342  eelT12  45344  eelTT1  45345  eelT01  45346  eel0T1  45347  uun132  45420  uun132p1  45421  un2122  45425  uunTT1  45428  uunTT1p1  45429  uunTT1p2  45430  uunT11  45431  uunT11p1  45432  uunT11p2  45433  uunT12  45434  uunT12p1  45435  uunT12p2  45436  uunT12p3  45437  uunT12p4  45438  uunT12p5  45439  uun111  45440  uun2221  45448  uun2221p1  45449  uun2221p2  45450  stoweidlem17  46658  stoweidlem34  46675  stoweidlem60  46701  ndmaovass  47867  ndmaovdistr  47868  4an21  47931  2elfz3nn0  47977  difltmodne  48009  prproropf1o  48180  fpprel  48417  clnbgredg  48529  dfvopnbgr2  48542  dfclnbgr6  48545  dfnbgr6  48546  dfsclnbgr6  48547  uhgrimprop  48581  isuspgrimlem  48584  clnbgrgrim  48623  isgrtri  48632  isubgr3stgrlem4  48658  isubgr3stgrlem7  48661  upwlksfval  48824  isupwlkg  48826  upwlkbprop  48827  2zrngnmrid  48945  lindslinindsimp2lem5  49162  i0oii  49618  io1ii  49619  sepnsepolem1  49620  isthincd2  50135  functhinc  50146  elpg  50412  alimp-no-surprise  50479