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  3501  ceqsex2v  3502  ceqsex3v  3503  ceqsex4v  3504  ceqsex6v  3505  ceqsex8v  3506  2reu5lem1  3726  2reu5lem2  3727  2reu5lem3  3728  eldifpr  4622  rexdifpr  4623  trel3  5224  2rbropap  5526  ordelord  6354  dflim2  6390  dff1o4  6808  foco2  7081  brfvopab  7446  eloprabga  7498  ndmovass  7577  ndmovdistr  7578  dflim3  7823  dflim4  7824  frxp2  8123  mpoxopovel  8199  dfsmo2  8316  dfrecs3  8341  oeeui  8566  naddasslem2  8659  ecopovtrn  8793  elixp2  8874  elixp  8877  mptelixpg  8908  dif1en  9124  dif1enOLD  9126  ssfi  9137  sbthfilem  9162  eqinf  9436  zorn2lem7  10455  grothprim  10787  grothtsk  10788  divmulasscom  11861  muldivdir  11875  divmuldiv  11882  sup3  12140  dfnn3  12200  prime  12615  eluz2  12799  raluz2  12856  elixx1  13315  elixx3g  13319  elioo2  13347  elioo5  13364  elicc4  13374  iccneg  13433  icoshft  13434  difreicc  13445  elfz1  13473  elfz  13474  elfz2  13475  elfzm11  13556  elfz2nn0  13579  elfzo2  13623  elfzo3  13637  lbfzo0  13660  fzo1lb  13674  1elfzo1  13675  fzind2  13746  zmodid2  13861  hashgt23el  14389  swrdnd2  14620  swrdnd0  14622  swrdccatin1  14690  swrdccat  14700  repswswrd  14749  swrdco  14803  2swrd2eqwrdeq  14919  rediv  15097  imdiv  15104  cosmul  16141  bitsval  16394  bitsmod  16406  bitscmp  16408  smueqlem  16460  dfgcd2  16516  lcmneg  16573  lcmftp  16606  coprmgcdb  16619  divgcdcoprmex  16636  cncongr1  16637  cncongr2  16638  difsqpwdvds  16858  oddprmdvds  16874  elgz  16902  xpsfrnel  17525  xpsfrnel2  17527  ismre  17551  mreexexlem4d  17608  iscatd2  17642  isssc  17782  eldmcoa  18027  isdrs  18262  isipodrs  18496  mgmsscl  18572  ismhm  18712  mhmpropd  18719  issubm  18730  issubmndb  18732  submacs  18754  issubg  19058  eqglact  19111  eqgid  19112  ecqusaddd  19124  ecqusaddcl  19125  pgrpsubgsymgbi  19338  isslw  19538  efgsdm  19660  mulgmhm  19757  mulgghm  19758  dmdprd  19930  dprdw  19942  subgdmdprd  19966  dmdprdpr  19981  isrng  20063  issrg  20097  srglmhm  20130  srgrmhm  20131  isring  20146  ringlghm  20221  dfrhm2  20383  issubrng  20456  issubrg3  20509  isdomn3  20624  issdrg  20697  sdrgacs  20710  islmod  20770  lsspropd  20924  islmhm  20934  islbs  20983  lbspropd  21006  qusmulrng  21192  rngqiprngghmlem3  21199  rngqiprnglinlem3  21203  rngqiprnglin  21212  cnfldfunALT  21279  cnfldfunALTOLD  21292  isphl  21537  elocv  21577  isobs  21629  mat1dimscm  22362  scmatghm  22420  scmatmhm  22421  ma1repvcl  22457  smadiadetr  22562  mat2pmatghm  22617  mat2pmatmul  22618  decpmatmulsumfsupp  22660  pm2mpghm  22703  pm2mpmhmlem1  22705  neindisj  23004  lmbrf  23147  hauscmplem  23293  llyi  23361  subislly  23368  islocfin  23404  uptx  23512  txcn  23513  qtopeu  23603  elmptrab  23714  isfbas  23716  trfil2  23774  flimcls  23872  cnextcn  23954  xmetec  24322  ngppropd  24525  ngpocelbl  24592  bl2ioo  24680  xrtgioo  24695  om1elbas  24932  elpi1  24945  isclm  24964  isclmp  24997  isncvsngp  25049  iscph  25070  tcphcph  25137  lmmbr2  25159  lmmbrf  25162  iscau2  25177  caussi  25197  lmclim  25203  bcthlem1  25224  srabn  25260  ishl2  25270  evthicc2  25361  ovolfioo  25368  ovolficc  25369  iblcnlem1  25689  iblrelem  25692  iblre  25695  iblcn  25700  isuc1p  26046  ismon1p  26048  ellogrn  26468  logreclem  26672  atandm  26786  atandm2  26787  atandm3  26788  atans2  26841  dmarea  26867  dchrelbas4  27154  lgsmodeq  27253  lgsmulsqcoprm  27254  nocvxminlem  27689  scutcut  27713  scutbday  27716  addscut2  27886  mulscut2  28036  ax5seg  28865  eengtrkg  28913  uspgredg2v  29151  nb3grpr2  29310  isrusgr0  29494  rusgrprop0  29495  ewlkprop  29531  wksfval  29537  wlkeq  29562  wlkson  29584  wlkonprop  29586  upgr2wlk  29596  upgrtrls  29629  upgristrl  29630  wksonproplem  29632  wksonproplemOLD  29633  pthsfval  29649  ispth  29651  dfpth2  29659  isspthonpth  29679  uhgrwkspth  29685  usgr2wlkspth  29689  crctcshwlkn0lem4  29743  wspthnp  29780  wwlknon  29787  wwlksnextwrd  29827  wwlksnextinj  29829  wspthsnwspthsnon  29846  umgr2adedgwlk  29875  umgr2adedgwlkon  29876  umgr2adedgwlkonALT  29877  umgr2adedgspth  29878  s3wwlks2on  29886  wpthswwlks2on  29891  usgr2wspthons3  29894  usgr2wspthon  29895  elwwlks2  29896  elwspths2spth  29897  rusgrnumwwlkl1  29898  rusgrnumwwlkslem  29899  isclwwlk  29913  clwwlkbp  29914  clwlkclwwlklem3  29930  isclwwlknx  29965  clwwlknp  29966  clwwlkn1  29970  clwwlkn2  29973  clwwlkwwlksb  29983  clwwlknonel  30024  0pth  30054  frcond4  30199  1to3vfriswmgr  30209  3cyclfrgr  30217  frgrwopreglem5  30250  2clwwlk2clwwlk  30279  numclwlk1lem1  30298  numclwwlk6  30319  ajval  30790  issh  31137  dmadjss  31816  adjeu  31818  adjval  31819  isst  32142  ishst  32143  xrdifh  32703  nndiffz1  32709  xdivpnfrp  32853  isomnd  33015  isslmd  33155  isprmidl  33409  isprmidlc  33418  ismxidl  33433  ressply1mon1p  33537  isrrext  33990  ismntop  34016  isros  34158  issros  34165  issibf  34324  eulerpartleme  34354  eulerpartlemt0  34360  probun  34410  bnj250  34691  bnj255  34695  bnj345  34704  bnj945  34763  bnj1209  34786  bnj1275  34803  bnj543  34883  bnj571  34896  bnj607  34906  bnj882  34916  bnj983  34941  bnj996  34946  bnj1006  34950  bnj1033  34959  bnj1097  34971  bnj1110  34972  bnj1145  34983  bnj1174  34993  bnj1189  34999  bnj1450  35040  bnj1514  35053  wevgblacfn  35096  cusgr3cyclex  35123  erdszelem1  35178  cvmsval  35253  cvmliftiota  35288  snmlval  35318  lediv2aALT  35664  elwlim  35811  brtxp2  35869  brpprod3a  35874  brcart  35920  brsuccf  35929  broutsideof3  36114  ivthALT  36323  df3nandALT2  36388  andnand1  36389  topdifinffinlem  37335  relowlssretop  37351  rdgeqoa  37358  unccur  37597  fin2solem  37600  poimirlem3  37617  poimirlem4  37618  poimirlem26  37640  poimirlem27  37641  poimirlem32  37646  itg2gt0cn  37669  iblabsnclem  37677  areacirc  37707  neificl  37747  ablo4pnp  37874  isrngohom  37959  isidl  38008  ispridl  38028  pridlidl  38029  ismaxidl  38034  maxidlidl  38035  isfldidl2  38063  isdmn3  38068  triantru3  38218  moantr  38346  brxrn2  38357  dfxrn2  38358  ecxrn  38373  disjressuc2  38374  inxpxrn  38381  rnxrn  38384  dmqsblocks  38845  islshp  38972  isopos  39173  cvrfval  39261  cvrval  39262  isatl  39292  isat3  39300  islpln5  39529  4atlem11  39603  dalem20  39687  lhpexle3  40006  lhpex2leN  40007  isltrn2N  40114  diclspsn  41188  lcfls1lem  41528  lcfls1N  41529  uzindd  41965  isprimroot  42081  flt4lem5e  42644  3cubes  42678  fz1eqin  42757  dflim6  43253  dflim7  43262  nnoeomeqom  43301  cantnfub2  43311  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  rp-isfinite6  43507  snhesn  43775  ismnuprim  44283  ismnushort  44290  iotasbc2  44409  eelT00  44694  eelTTT  44695  eelT11  44696  eelT12  44698  eelTT1  44699  eelT01  44700  eel0T1  44701  uun132  44774  uun132p1  44775  un2122  44779  uunTT1  44782  uunTT1p1  44783  uunTT1p2  44784  uunT11  44785  uunT11p1  44786  uunT11p2  44787  uunT12  44788  uunT12p1  44789  uunT12p2  44790  uunT12p3  44791  uunT12p4  44792  uunT12p5  44793  uun111  44794  uun2221  44802  uun2221p1  44803  uun2221p2  44804  stoweidlem17  46015  stoweidlem34  46032  stoweidlem60  46058  ndmaovass  47207  ndmaovdistr  47208  4an21  47271  2elfz3nn0  47317  difltmodne  47343  prproropf1o  47508  fpprel  47729  clnbgredg  47840  dfvopnbgr2  47853  dfclnbgr6  47856  dfnbgr6  47857  dfsclnbgr6  47858  uhgrimprop  47892  isuspgrimlem  47895  clnbgrgrim  47934  isgrtri  47942  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  upwlksfval  48123  isupwlkg  48125  upwlkbprop  48126  2zrngnmrid  48244  lindslinindsimp2lem5  48451  i0oii  48908  io1ii  48909  sepnsepolem1  48910  isthincd2  49426  functhinc  49437  elpg  49703  alimp-no-surprise  49770