MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anass Structured version   Visualization version   GIF version

Theorem 3anass 1040
Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anass ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))

Proof of Theorem 3anass
StepHypRef Expression
1 df-3an 1038 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 680 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  3anrot  1041  3anan12  1049  anandi3  1050  3biant1d  1438  an33rean  1443  cad1  1552  3exdistr  1920  ceqsex2  3234  ceqsex3v  3236  ceqsex4v  3237  ceqsex6v  3238  ceqsex8v  3239  2reu5lem1  3400  2reu5lem2  3401  2reu5lem3  3402  eldifpr  4182  rexdifpr  4183  trel3  4730  2rbropap  4987  ordelord  5714  dflim2  5750  dff1o4  6112  foco2  6345  brfvopab  6665  ndmovass  6787  ndmovdistr  6788  dflim3  7009  dflim4  7010  mpt2xopovel  7306  dfsmo2  7404  dfrecs3  7429  oeeui  7642  ecopovtrn  7810  elixp2  7872  elixp  7875  mptelixpg  7905  eqinf  8350  zorn2lem7  9284  grothprim  9616  grothtsk  9617  divmulasscom  10669  muldivdir  10680  divmuldiv  10685  sup3  10940  dfnn3  10994  prime  11418  eluz2  11653  raluz2  11697  elixx1  12142  elixx3g  12146  elioo2  12174  elioo5  12189  elicc4  12198  iccneg  12251  icoshft  12252  difreicc  12262  elfz1  12289  elfz  12290  elfz2  12291  elfzm11  12368  elfz2nn0  12388  elfzo2  12430  elfzo3  12443  lbfzo0  12464  fzind2  12542  zmodid2  12654  swrdnd2  13387  swrdccatin1  13436  swrdccat  13446  repswswrd  13484  swrdco  13536  2swrd2eqwrdeq  13646  ccat2s1fvwALT  13648  rediv  13821  imdiv  13828  cosmul  14847  bitsval  15089  bitsmod  15101  bitscmp  15103  smueqlem  15155  dfgcd2  15206  lcmneg  15259  lcmftp  15292  coprmgcdb  15305  divgcdcoprmex  15323  cncongr1  15324  cncongr2  15325  difsqpwdvds  15534  oddprmdvds  15550  elgz  15578  xpsfrnel  16163  xpsfrnel2  16165  ismre  16190  mreexexlem4d  16247  iscatd2  16282  isssc  16420  eldmcoa  16655  isdrs  16874  isipodrs  17101  ismhm  17277  mhmpropd  17281  issubm  17287  submacs  17305  issubg  17534  eqglact  17585  eqgid  17586  pgrpsubgsymgbi  17767  isslw  17963  efgsdm  18083  mulgmhm  18173  mulgghm  18174  dmdprd  18337  dprdw  18349  subgdmdprd  18373  dmdprdpr  18388  issrg  18447  srglmhm  18475  srgrmhm  18476  isring  18491  ringlghm  18544  dfrhm2  18657  issubrg3  18748  islmod  18807  lsspropd  18957  islmhm  18967  islbs  19016  lbspropd  19039  isphl  19913  elocv  19952  isobs  20004  mat1dimscm  20221  scmatghm  20279  scmatmhm  20280  ma1repvcl  20316  smadiadetr  20421  mat2pmatghm  20475  mat2pmatmul  20476  decpmatmulsumfsupp  20518  pm2mpghm  20561  pm2mpmhmlem1  20563  neindisj  20861  lmbrf  21004  hauscmplem  21149  llyi  21217  subislly  21224  islocfin  21260  uptx  21368  txcn  21369  qtopeu  21459  elmptrab  21570  isfbas  21573  trfil2  21631  flimcls  21729  cnextcn  21811  xmetec  22179  ngppropd  22381  ngpocelbl  22448  bl2ioo  22535  xrtgioo  22549  om1elbas  22772  elpi1  22785  isclm  22804  isclmp  22837  isncvsngp  22889  iscph  22910  tchcph  22976  lmmbr2  22997  lmmbrf  23000  iscau2  23015  caussi  23035  lmclim  23041  bcthlem1  23061  srabn  23096  ishl2  23106  evthicc2  23169  ovolfioo  23176  ovolficc  23177  iblcnlem1  23494  iblrelem  23497  iblre  23500  iblcn  23505  isuc1p  23838  ismon1p  23840  ellogrn  24244  logreclem  24434  atandm  24537  atandm2  24538  atandm3  24539  atans2  24592  dmarea  24618  dchrelbas4  24902  lgsmodeq  25001  lgsmulsqcoprm  25002  ax5seg  25752  eengtrkg  25799  uspgredg2v  26043  nbgrel  26159  nb3grpr2  26206  isrusgr0  26366  rusgrprop0  26367  ewlkprop  26403  wksfval  26409  wlkeq  26433  wlkson  26455  wlkonprop  26457  upgr2wlk  26467  upgrtrls  26501  upgristrl  26502  wksonproplem  26504  pthsfval  26520  ispth  26522  isspthonpth  26548  uhgrwkspth  26554  usgr2wlkspth  26558  crctcshwlkn0lem4  26608  wspthnp  26640  wwlknon  26645  wwlksnextwrd  26695  wwlksnextinj  26697  wspthsnwspthsnon  26714  umgr2adedgwlk  26744  umgr2adedgwlkon  26745  umgr2adedgwlkonALT  26746  umgr2adedgspth  26747  s3wwlks2on  26752  wpthswwlks2on  26756  usgr2wspthons3  26759  usgr2wspthon  26760  elwwlks2  26762  elwspths2spth  26763  rusgrnumwwlkl1  26764  rusgrnumwwlkslem  26765  isclwwlks  26781  clwwlkbp  26784  clwwlknp  26788  isclwwlksnx  26790  clwlkclwwlklem3  26803  clwwlksn2  26810  clwlksfclwwlk  26862  0pth  26886  1to3vfriswmgr  27042  3cyclfrgr  27050  numclwwlkovgel  27111  numclwwlk6  27136  ajval  27605  issh  27953  dmadjss  28634  adjeu  28636  adjval  28637  isst  28960  ishst  28961  xrdifh  29427  nndiffz1  29431  xdivpnfrp  29468  isomnd  29528  isslmd  29582  isrrext  29868  ismntop  29894  isros  30054  issros  30061  issibf  30218  eulerpartleme  30248  eulerpartlemt0  30254  probun  30304  bnj250  30527  bnj255  30531  bnj345  30540  bnj945  30605  bnj1209  30628  bnj1275  30645  bnj543  30724  bnj571  30737  bnj607  30747  bnj882  30757  bnj983  30782  bnj996  30786  bnj1006  30790  bnj1033  30798  bnj1097  30810  bnj1110  30811  bnj1145  30822  bnj1174  30832  bnj1189  30838  bnj1450  30879  bnj1514  30892  erdszelem1  30934  cvmsval  31009  cvmliftiota  31044  snmlval  31074  lediv2aALT  31332  elwlim  31523  elwlimOLD  31524  nocvxminlem  31606  brtxp2  31683  brpprod3a  31688  brcart  31734  brsuccf  31743  broutsideof3  31928  ivthALT  32025  df3nandALT2  32092  andnand1  32093  topdifinffinlem  32866  relowlssretop  32882  rdgeqoa  32889  unccur  33063  fin2solem  33066  poimirlem3  33083  poimirlem4  33084  poimirlem26  33106  poimirlem27  33107  poimirlem32  33112  itg2gt0cn  33136  iblabsnclem  33144  areacirc  33176  neificl  33220  ablo4pnp  33350  isrngohom  33435  isidl  33484  ispridl  33504  pridlidl  33505  ismaxidl  33510  maxidlidl  33511  isfldidl2  33539  isdmn3  33544  islshp  33785  isopos  33986  cvrfval  34074  cvrval  34075  isatl  34105  isat3  34113  islpln5  34340  4atlem11  34414  dalem20  34498  lhpexle3  34817  lhpex2leN  34818  isltrn2N  34925  diclspsn  36002  lcfls1lem  36342  lcfls1N  36343  fz1eqin  36851  issdrg  37287  sdrgacs  37291  isdomn3  37302  rp-isfinite6  37384  snhesn  37601  iotasbc2  38142  eelT00  38451  eelTTT  38452  eelT11  38453  eelT12  38455  eelTT1  38456  eelT01  38457  eel0T1  38458  uun132  38533  uun132p1  38534  un2122  38538  uunTT1  38541  uunTT1p1  38542  uunTT1p2  38543  uunT11  38544  uunT11p1  38545  uunT11p2  38546  uunT12  38547  uunT12p1  38548  uunT12p2  38549  uunT12p3  38550  uunT12p4  38551  uunT12p5  38552  uun111  38553  uun2221  38561  uun2221p1  38562  uun2221p2  38563  stoweidlem17  39571  stoweidlem34  39588  stoweidlem60  39614  ndmaovass  40620  ndmaovdistr  40621  2elfz3nn0  40653  reuccatpfxs1  40763  upwlksfval  41034  isupwlkg  41036  upwlkbprop  41037  isrng  41194  2zrngnmrid  41268  lindslinindsimp2lem5  41569  elpg  41780  alimp-no-surprise  41860
  Copyright terms: Public domain W3C validator