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  3751  2reu5lem2  3752  2reu5lem3  3753  eldifpr  4660  rexdifpr  4661  trel3  5275  2rbropap  5566  ordelord  6384  dflim2  6419  dff1o4  6839  foco2  7106  brfvopab  7463  eloprabga  7513  ndmovass  7592  ndmovdistr  7593  dflim3  7833  dflim4  7834  frxp2  8127  mpoxopovel  8202  dfsmo2  8344  dfrecs3  8369  dfrecs3OLD  8370  oeeui  8599  naddasslem2  8691  ecopovtrn  8811  elixp2  8892  elixp  8895  mptelixpg  8926  dif1en  9157  dif1enOLD  9159  ssfi  9170  sbthfilem  9198  eqinf  9476  zorn2lem7  10494  grothprim  10826  grothtsk  10827  divmulasscom  11893  muldivdir  11904  divmuldiv  11911  sup3  12168  dfnn3  12223  prime  12640  eluz2  12825  raluz2  12878  elixx1  13330  elixx3g  13334  elioo2  13362  elioo5  13378  elicc4  13388  iccneg  13446  icoshft  13447  difreicc  13458  elfz1  13486  elfz  13487  elfz2  13488  elfzm11  13569  elfz2nn0  13589  elfzo2  13632  elfzo3  13646  lbfzo0  13669  fzind2  13747  zmodid2  13861  hashgt23el  14381  swrdnd2  14602  swrdnd0  14604  swrdccatin1  14672  swrdccat  14682  repswswrd  14731  swrdco  14785  2swrd2eqwrdeq  14901  rediv  15075  imdiv  15082  cosmul  16113  bitsval  16362  bitsmod  16374  bitscmp  16376  smueqlem  16428  dfgcd2  16485  lcmneg  16537  lcmftp  16570  coprmgcdb  16583  divgcdcoprmex  16600  cncongr1  16601  cncongr2  16602  difsqpwdvds  16817  oddprmdvds  16833  elgz  16861  xpsfrnel  17505  xpsfrnel2  17507  ismre  17531  mreexexlem4d  17588  iscatd2  17622  isssc  17764  eldmcoa  18012  isdrs  18251  isipodrs  18487  mgmsscl  18563  ismhm  18670  mhmpropd  18675  issubm  18681  issubmndb  18683  submacs  18705  issubg  19001  eqglact  19054  eqgid  19055  pgrpsubgsymgbi  19271  isslw  19471  efgsdm  19593  mulgmhm  19690  mulgghm  19691  dmdprd  19863  dprdw  19875  subgdmdprd  19899  dmdprdpr  19914  issrg  20005  srglmhm  20038  srgrmhm  20039  isring  20054  ringlghm  20118  dfrhm2  20246  issubrg3  20385  issdrg  20397  sdrgacs  20410  islmod  20468  lsspropd  20621  islmhm  20631  islbs  20680  lbspropd  20703  cnfldfunALT  20950  isphl  21173  elocv  21213  isobs  21267  mat1dimscm  21969  scmatghm  22027  scmatmhm  22028  ma1repvcl  22064  smadiadetr  22169  mat2pmatghm  22224  mat2pmatmul  22225  decpmatmulsumfsupp  22267  pm2mpghm  22310  pm2mpmhmlem1  22312  neindisj  22613  lmbrf  22756  hauscmplem  22902  llyi  22970  subislly  22977  islocfin  23013  uptx  23121  txcn  23122  qtopeu  23212  elmptrab  23323  isfbas  23325  trfil2  23383  flimcls  23481  cnextcn  23563  xmetec  23932  ngppropd  24138  ngpocelbl  24213  bl2ioo  24300  xrtgioo  24314  om1elbas  24540  elpi1  24553  isclm  24572  isclmp  24605  isncvsngp  24658  iscph  24679  tcphcph  24746  lmmbr2  24768  lmmbrf  24771  iscau2  24786  caussi  24806  lmclim  24812  bcthlem1  24833  srabn  24869  ishl2  24879  evthicc2  24969  ovolfioo  24976  ovolficc  24977  iblcnlem1  25297  iblrelem  25300  iblre  25303  iblcn  25308  isuc1p  25650  ismon1p  25652  ellogrn  26060  logreclem  26257  atandm  26371  atandm2  26372  atandm3  26373  atans2  26426  dmarea  26452  dchrelbas4  26736  lgsmodeq  26835  lgsmulsqcoprm  26836  nocvxminlem  27269  scutcut  27292  scutbday  27295  addscut2  27453  mulscut2  27579  ax5seg  28186  eengtrkg  28234  uspgredg2v  28471  nb3grpr2  28630  isrusgr0  28813  rusgrprop0  28814  ewlkprop  28850  wksfval  28856  wlkeq  28881  wlkson  28903  wlkonprop  28905  upgr2wlk  28915  upgrtrls  28948  upgristrl  28949  wksonproplem  28951  wksonproplemOLD  28952  pthsfval  28968  ispth  28970  isspthonpth  28996  uhgrwkspth  29002  usgr2wlkspth  29006  crctcshwlkn0lem4  29057  wspthnp  29094  wwlknon  29101  wwlksnextwrd  29141  wwlksnextinj  29143  wspthsnwspthsnon  29160  umgr2adedgwlk  29189  umgr2adedgwlkon  29190  umgr2adedgwlkonALT  29191  umgr2adedgspth  29192  s3wwlks2on  29200  wpthswwlks2on  29205  usgr2wspthons3  29208  usgr2wspthon  29209  elwwlks2  29210  elwspths2spth  29211  rusgrnumwwlkl1  29212  rusgrnumwwlkslem  29213  isclwwlk  29227  clwwlkbp  29228  clwlkclwwlklem3  29244  isclwwlknx  29279  clwwlknp  29280  clwwlkn1  29284  clwwlkn2  29287  clwwlkwwlksb  29297  clwwlknonel  29338  0pth  29368  frcond4  29513  1to3vfriswmgr  29523  3cyclfrgr  29531  frgrwopreglem5  29564  2clwwlk2clwwlk  29593  numclwlk1lem1  29612  numclwwlk6  29633  ajval  30102  issh  30449  dmadjss  31128  adjeu  31130  adjval  31131  isst  31454  ishst  31455  xrdifh  31979  nndiffz1  31985  xdivpnfrp  32087  isomnd  32207  isslmd  32335  isprmidl  32545  isprmidlc  32555  ismxidl  32567  ressply1mon1p  32646  isrrext  32969  ismntop  32995  isros  33155  issros  33162  issibf  33321  eulerpartleme  33351  eulerpartlemt0  33357  probun  33407  bnj250  33701  bnj255  33705  bnj345  33714  bnj945  33773  bnj1209  33796  bnj1275  33813  bnj543  33893  bnj571  33906  bnj607  33916  bnj882  33926  bnj983  33951  bnj996  33956  bnj1006  33960  bnj1033  33969  bnj1097  33981  bnj1110  33982  bnj1145  33993  bnj1174  34003  bnj1189  34009  bnj1450  34050  bnj1514  34063  cusgr3cyclex  34116  erdszelem1  34171  cvmsval  34246  cvmliftiota  34281  snmlval  34311  lediv2aALT  34651  elwlim  34784  brtxp2  34842  brpprod3a  34847  brcart  34893  brsuccf  34902  broutsideof3  35087  ivthALT  35209  df3nandALT2  35274  andnand1  35275  topdifinffinlem  36217  relowlssretop  36233  rdgeqoa  36240  unccur  36460  fin2solem  36463  poimirlem3  36480  poimirlem4  36481  poimirlem26  36503  poimirlem27  36504  poimirlem32  36509  itg2gt0cn  36532  iblabsnclem  36540  areacirc  36570  neificl  36610  ablo4pnp  36737  isrngohom  36822  isidl  36871  ispridl  36891  pridlidl  36892  ismaxidl  36897  maxidlidl  36898  isfldidl2  36926  isdmn3  36931  triantru3  37083  moantr  37222  brxrn2  37234  dfxrn2  37235  ecxrn  37246  disjressuc2  37247  inxpxrn  37254  rnxrn  37257  islshp  37838  isopos  38039  cvrfval  38127  cvrval  38128  isatl  38158  isat3  38166  islpln5  38395  4atlem11  38469  dalem20  38553  lhpexle3  38872  lhpex2leN  38873  isltrn2N  38980  diclspsn  40054  lcfls1lem  40394  lcfls1N  40395  uzindd  40831  flt4lem5e  41395  3cubes  41414  fz1eqin  41493  isdomn3  41932  dflim6  42000  dflim7  42009  nnoeomeqom  42048  cantnfub2  42058  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  rp-isfinite6  42255  snhesn  42523  ismnuprim  43039  ismnushort  43046  iotasbc2  43165  eelT00  43452  eelTTT  43453  eelT11  43454  eelT12  43456  eelTT1  43457  eelT01  43458  eel0T1  43459  uun132  43532  uun132p1  43533  un2122  43537  uunTT1  43540  uunTT1p1  43541  uunTT1p2  43542  uunT11  43543  uunT11p1  43544  uunT11p2  43545  uunT12  43546  uunT12p1  43547  uunT12p2  43548  uunT12p3  43549  uunT12p4  43550  uunT12p5  43551  uun111  43552  uun2221  43560  uun2221p1  43561  uun2221p2  43562  stoweidlem17  44720  stoweidlem34  44737  stoweidlem60  44763  ndmaovass  45901  ndmaovdistr  45902  4an21  45965  2elfz3nn0  46011  prproropf1o  46162  fpprel  46383  upwlksfval  46500  isupwlkg  46502  upwlkbprop  46503  isrng  46637  issubrng  46711  ecqusadd  46750  ecqusaddcl  46751  qusmulrng  46752  rngqiprngghmlem3  46755  rngqiprnglinlem3  46759  rngqiprnglin  46768  2zrngnmrid  46802  lindslinindsimp2lem5  47097  i0oii  47506  io1ii  47507  sepnsepolem1  47508  iscnrm3lem3  47522  isthincd2  47612  functhinc  47619  elpg  47713  alimp-no-surprise  47782