Theorem 3anass 1095

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

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

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 1089

This theorem is referenced by:  3anan12  1096  3ancoma  1098  anandi3  1102  4anpull2  1363  3biant1d  1481  an33rean  1486  cad1  1619  3exdistr  1962  ceqsex2  3495  ceqsex2v  3496  ceqsex3v  3497  ceqsex4v  3498  ceqsex6v  3499  ceqsex8v  3500  2reu5lem1  3715  2reu5lem2  3716  2reu5lem3  3717  eldifpr  4617  rexdifpr  4618  trel3  5216  2rbropap  5522  ordelord  6349  dflim2  6385  dff1o4  6792  foco2  7065  brfvopab  7427  eloprabga  7479  ndmovass  7558  ndmovdistr  7559  dflim3  7801  dflim4  7802  frxp2  8098  mpoxopovel  8174  dfsmo2  8291  dfrecs3  8316  oeeui  8542  naddasslem2  8635  ecopovtrn  8771  elixp2  8853  elixp  8856  mptelixpg  8887  dif1en  9100  ssfi  9111  sbthfilem  9136  eqinf  9402  zorn2lem7  10426  grothprim  10759  grothtsk  10760  divmulasscom  11834  muldivdir  11848  divmuldiv  11855  sup3  12113  dfnn3  12173  prime  12587  eluz2  12771  raluz2  12824  elixx1  13284  elixx3g  13288  elioo2  13316  elioo5  13333  elicc4  13343  iccneg  13402  icoshft  13403  difreicc  13414  elfz1  13442  elfz  13443  elfz2  13444  elfzm11  13525  elfz2nn0  13548  elfzo2  13592  elfzo3  13606  lbfzo0  13629  fzo1lb  13643  1elfzo1  13644  fzind2  13718  zmodid2  13833  hashgt23el  14361  swrdnd2  14593  swrdnd0  14595  swrdccatin1  14662  swrdccat  14672  repswswrd  14721  swrdco  14774  2swrd2eqwrdeq  14890  rediv  15068  imdiv  15075  cosmul  16112  bitsval  16365  bitsmod  16377  bitscmp  16379  smueqlem  16431  dfgcd2  16487  lcmneg  16544  lcmftp  16577  coprmgcdb  16590  divgcdcoprmex  16607  cncongr1  16608  cncongr2  16609  difsqpwdvds  16829  oddprmdvds  16845  elgz  16873  xpsfrnel  17497  xpsfrnel2  17499  ismre  17523  mreexexlem4d  17584  iscatd2  17618  isssc  17758  eldmcoa  18003  isdrs  18238  isipodrs  18474  mgmsscl  18584  ismhm  18724  mhmpropd  18731  issubm  18742  issubmndb  18744  submacs  18766  issubg  19073  eqglact  19125  eqgid  19126  ecqusaddd  19138  ecqusaddcl  19139  pgrpsubgsymgbi  19354  isslw  19554  efgsdm  19676  mulgmhm  19773  mulgghm  19774  dmdprd  19946  dprdw  19958  subgdmdprd  19982  dmdprdpr  19997  isomnd  20069  isrng  20106  issrg  20140  srglmhm  20173  srgrmhm  20174  isring  20189  ringlghm  20264  dfrhm2  20427  issubrng  20497  issubrg3  20550  isdomn3  20665  issdrg  20738  sdrgacs  20751  islmod  20832  lsspropd  20986  islmhm  20996  islbs  21045  lbspropd  21068  qusmulrng  21254  rngqiprngghmlem3  21261  rngqiprnglinlem3  21265  rngqiprnglin  21274  cnfldfunALT  21341  cnfldfunALTOLD  21354  isphl  21600  elocv  21640  isobs  21692  mat1dimscm  22436  scmatghm  22494  scmatmhm  22495  ma1repvcl  22531  smadiadetr  22636  mat2pmatghm  22691  mat2pmatmul  22692  decpmatmulsumfsupp  22734  pm2mpghm  22777  pm2mpmhmlem1  22779  neindisj  23078  lmbrf  23221  hauscmplem  23367  llyi  23435  subislly  23442  islocfin  23478  uptx  23586  txcn  23587  qtopeu  23677  elmptrab  23788  isfbas  23790  trfil2  23848  flimcls  23946  cnextcn  24028  xmetec  24395  ngppropd  24598  ngpocelbl  24665  bl2ioo  24753  xrtgioo  24768  om1elbas  25005  elpi1  25018  isclm  25037  isclmp  25070  isncvsngp  25122  iscph  25143  tcphcph  25210  lmmbr2  25232  lmmbrf  25235  iscau2  25250  caussi  25270  lmclim  25276  bcthlem1  25297  srabn  25333  ishl2  25343  evthicc2  25434  ovolfioo  25441  ovolficc  25442  iblcnlem1  25762  iblrelem  25765  iblre  25768  iblcn  25773  isuc1p  26119  ismon1p  26121  ellogrn  26541  logreclem  26745  atandm  26859  atandm2  26860  atandm3  26861  atans2  26914  dmarea  26940  dchrelbas4  27227  lgsmodeq  27326  lgsmulsqcoprm  27327  nocvxminlem  27767  cutcuts  27794  cutbday  27797  addcuts2  27992  mulcut2  28146  ax5seg  29029  eengtrkg  29077  uspgredg2v  29315  nb3grpr2  29474  isrusgr0  29658  rusgrprop0  29659  ewlkprop  29695  wksfval  29701  wlkeq  29725  wlkson  29746  wlkonprop  29748  upgr2wlk  29758  upgrtrls  29791  upgristrl  29792  wksonproplem  29794  pthsfval  29810  ispth  29812  dfpth2  29820  isspthonpth  29840  uhgrwkspth  29846  usgr2wlkspth  29850  crctcshwlkn0lem4  29904  wspthnp  29941  wwlknon  29948  wwlksnextwrd  29988  wwlksnextinj  29990  wspthsnwspthsnon  30007  umgr2adedgwlk  30036  umgr2adedgwlkon  30037  umgr2adedgwlkonALT  30038  umgr2adedgspth  30039  s3wwlks2on  30047  sps3wwlks2on  30048  wpthswwlks2on  30055  usgr2wspthons3  30058  usgr2wspthon  30059  elwwlks2  30060  elwspths2spth  30061  rusgrnumwwlkl1  30062  rusgrnumwwlkslem  30063  isclwwlk  30077  clwwlkbp  30078  clwlkclwwlklem3  30094  isclwwlknx  30129  clwwlknp  30130  clwwlkn1  30134  clwwlkn2  30137  clwwlkwwlksb  30147  clwwlknonel  30188  0pth  30218  frcond4  30363  1to3vfriswmgr  30373  3cyclfrgr  30381  frgrwopreglem5  30414  2clwwlk2clwwlk  30443  numclwlk1lem1  30462  numclwwlk6  30483  ajval  30955  issh  31302  dmadjss  31981  adjeu  31983  adjval  31984  isst  32307  ishst  32308  xrdifh  32877  nndiffz1  32883  xdivpnfrp  33031  isslmd  33302  isprmidl  33537  isprmidlc  33546  ismxidl  33561  ressply1mon1p  33667  isrrext  34184  ismntop  34210  isros  34352  issros  34359  issibf  34517  eulerpartleme  34547  eulerpartlemt0  34553  probun  34603  bnj250  34884  bnj255  34888  bnj345  34897  bnj945  34956  bnj1209  34978  bnj1275  34995  bnj543  35075  bnj571  35088  bnj607  35098  bnj882  35108  bnj983  35133  bnj996  35138  bnj1006  35142  bnj1033  35151  bnj1097  35163  bnj1110  35164  bnj1145  35175  bnj1174  35185  bnj1189  35191  bnj1450  35232  bnj1514  35245  axprALT2  35293  wevgblacfn  35331  cusgr3cyclex  35358  erdszelem1  35413  cvmsval  35488  cvmliftiota  35523  snmlval  35553  lediv2aALT  35899  elwlim  36043  brtxp2  36101  brpprod3a  36106  brcart  36152  lemsuccf  36161  broutsideof3  36348  ivthALT  36557  df3nandALT2  36622  andnand1  36623  topdifinffinlem  37629  relowlssretop  37645  rdgeqoa  37652  unccur  37883  fin2solem  37886  poimirlem3  37903  poimirlem4  37904  poimirlem26  37926  poimirlem27  37927  poimirlem32  37932  itg2gt0cn  37955  iblabsnclem  37963  areacirc  37993  neificl  38033  ablo4pnp  38160  isrngohom  38245  isidl  38294  ispridl  38314  pridlidl  38315  ismaxidl  38320  maxidlidl  38321  isfldidl2  38349  isdmn3  38354  triantru3  38516  moantr  38652  brxrn2  38664  dfxrn2  38665  ecxrn  38686  disjressuc2  38691  inxpxrn  38698  rnxrn  38701  dfsuccl4  38754  dmqsblocks  39247  islshp  39384  isopos  39585  cvrfval  39673  cvrval  39674  isatl  39704  isat3  39712  islpln5  39940  4atlem11  40014  dalem20  40098  lhpexle3  40417  lhpex2leN  40418  isltrn2N  40525  diclspsn  41599  lcfls1lem  41939  lcfls1N  41940  uzindd  42376  isprimroot  42492  flt4lem5e  43043  3cubes  43076  fz1eqin  43155  dflim6  43650  dflim7  43659  nnoeomeqom  43698  cantnfub2  43708  fzunt  43840  fzuntd  43841  fzunt1d  43842  fzuntgd  43843  rp-isfinite6  43903  snhesn  44171  ismnuprim  44679  ismnushort  44686  iotasbc2  44805  eelT00  45089  eelTTT  45090  eelT11  45091  eelT12  45093  eelTT1  45094  eelT01  45095  eel0T1  45096  uun132  45169  uun132p1  45170  un2122  45174  uunTT1  45177  uunTT1p1  45178  uunTT1p2  45179  uunT11  45180  uunT11p1  45181  uunT11p2  45182  uunT12  45183  uunT12p1  45184  uunT12p2  45185  uunT12p3  45186  uunT12p4  45187  uunT12p5  45188  uun111  45189  uun2221  45197  uun2221p1  45198  uun2221p2  45199  stoweidlem17  46404  stoweidlem34  46421  stoweidlem60  46447  ndmaovass  47595  ndmaovdistr  47596  4an21  47659  2elfz3nn0  47705  difltmodne  47731  prproropf1o  47896  fpprel  48117  clnbgredg  48229  dfvopnbgr2  48242  dfclnbgr6  48245  dfnbgr6  48246  dfsclnbgr6  48247  uhgrimprop  48281  isuspgrimlem  48284  clnbgrgrim  48323  isgrtri  48332  isubgr3stgrlem4  48358  isubgr3stgrlem7  48361  upwlksfval  48524  isupwlkg  48526  upwlkbprop  48527  2zrngnmrid  48645  lindslinindsimp2lem5  48851  i0oii  49308  io1ii  49309  sepnsepolem1  49310  isthincd2  49825  functhinc  49836  elpg  50102  alimp-no-surprise  50169