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

Theorem 3anass 1092
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 1086 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 472 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 278 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1084
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 400  df-3an 1086
This theorem is referenced by:  3anan12  1093  3ancoma  1095  anandi3  1099  3biant1d  1475  an33rean  1480  an33reanOLD  1481  cad1  1618  3exdistr  1962  ceqsex2  3494  ceqsex2v  3495  ceqsex3v  3496  ceqsex4v  3497  ceqsex6v  3498  ceqsex8v  3499  2reu5lem1  3697  2reu5lem2  3698  2reu5lem3  3699  eldifpr  4560  rexdifpr  4561  trel3  5147  2rbropap  5419  ordelord  6185  dflim2  6219  dff1o4  6602  foco2  6854  brfvopab  7194  ndmovass  7320  ndmovdistr  7321  dflim3  7546  dflim4  7547  mpoxopovel  7873  dfsmo2  7971  dfrecs3  7996  oeeui  8215  ecopovtrn  8387  elixp2  8452  elixp  8455  mptelixpg  8486  eqinf  8936  zorn2lem7  9917  grothprim  10249  grothtsk  10250  divmulasscom  11315  muldivdir  11326  divmuldiv  11333  sup3  11589  dfnn3  11643  prime  12055  eluz2  12241  raluz2  12289  elixx1  12739  elixx3g  12743  elioo2  12771  elioo5  12786  elicc4  12796  iccneg  12854  icoshft  12855  difreicc  12866  elfz1  12894  elfz  12895  elfz2  12896  elfzm11  12977  elfz2nn0  12997  elfzo2  13040  elfzo3  13053  lbfzo0  13076  fzind2  13154  zmodid2  13266  hashgt23el  13785  swrdnd2  14012  swrdnd0  14014  swrdccatin1  14082  swrdccat  14092  repswswrd  14141  swrdco  14194  2swrd2eqwrdeq  14310  ccat2s1fvwALTOLD  14314  rediv  14485  imdiv  14492  cosmul  15521  bitsval  15766  bitsmod  15778  bitscmp  15780  smueqlem  15832  dfgcd2  15887  lcmneg  15940  lcmftp  15973  coprmgcdb  15986  divgcdcoprmex  16003  cncongr1  16004  cncongr2  16005  difsqpwdvds  16216  oddprmdvds  16232  elgz  16260  xpsfrnel  16830  xpsfrnel2  16832  ismre  16856  mreexexlem4d  16913  iscatd2  16947  isssc  17085  eldmcoa  17320  isdrs  17539  isipodrs  17766  mgmsscl  17852  ismhm  17953  mhmpropd  17957  issubm  17963  issubmndb  17965  submacs  17986  issubg  18274  eqglact  18326  eqgid  18327  pgrpsubgsymgbi  18531  isslw  18728  efgsdm  18851  mulgmhm  18944  mulgghm  18945  dmdprd  19116  dprdw  19128  subgdmdprd  19152  dmdprdpr  19167  issrg  19253  srglmhm  19281  srgrmhm  19282  isring  19297  ringlghm  19353  dfrhm2  19468  issubrg3  19559  issdrg  19570  sdrgacs  19576  islmod  19634  lsspropd  19785  islmhm  19795  islbs  19844  lbspropd  19867  isphl  20320  elocv  20360  isobs  20412  mat1dimscm  21083  scmatghm  21141  scmatmhm  21142  ma1repvcl  21178  smadiadetr  21283  mat2pmatghm  21338  mat2pmatmul  21339  decpmatmulsumfsupp  21381  pm2mpghm  21424  pm2mpmhmlem1  21426  neindisj  21725  lmbrf  21868  hauscmplem  22014  llyi  22082  subislly  22089  islocfin  22125  uptx  22233  txcn  22234  qtopeu  22324  elmptrab  22435  isfbas  22437  trfil2  22495  flimcls  22593  cnextcn  22675  xmetec  23044  ngppropd  23246  ngpocelbl  23313  bl2ioo  23400  xrtgioo  23414  om1elbas  23640  elpi1  23653  isclm  23672  isclmp  23705  isncvsngp  23757  iscph  23778  tcphcph  23844  lmmbr2  23866  lmmbrf  23869  iscau2  23884  caussi  23904  lmclim  23910  bcthlem1  23931  srabn  23967  ishl2  23977  evthicc2  24067  ovolfioo  24074  ovolficc  24075  iblcnlem1  24394  iblrelem  24397  iblre  24400  iblcn  24405  isuc1p  24744  ismon1p  24746  ellogrn  25154  logreclem  25351  atandm  25465  atandm2  25466  atandm3  25467  atans2  25520  dmarea  25546  dchrelbas4  25830  lgsmodeq  25929  lgsmulsqcoprm  25930  ax5seg  26735  eengtrkg  26783  uspgredg2v  27017  nb3grpr2  27176  isrusgr0  27359  rusgrprop0  27360  ewlkprop  27396  wksfval  27402  wlkeq  27426  wlkson  27449  wlkonprop  27451  upgr2wlk  27461  upgrtrls  27494  upgristrl  27495  wksonproplem  27497  pthsfval  27513  ispth  27515  isspthonpth  27541  uhgrwkspth  27547  usgr2wlkspth  27551  crctcshwlkn0lem4  27602  wspthnp  27639  wwlknon  27646  wwlksnextwrd  27686  wwlksnextinj  27688  wspthsnwspthsnon  27705  umgr2adedgwlk  27734  umgr2adedgwlkon  27735  umgr2adedgwlkonALT  27736  umgr2adedgspth  27737  s3wwlks2on  27745  wpthswwlks2on  27750  usgr2wspthons3  27753  usgr2wspthon  27754  elwwlks2  27755  elwspths2spth  27756  rusgrnumwwlkl1  27757  rusgrnumwwlkslem  27758  isclwwlk  27772  clwwlkbp  27773  clwlkclwwlklem3  27789  isclwwlknx  27824  clwwlknp  27825  clwwlkn1  27829  clwwlkn2  27832  clwwlkwwlksb  27842  clwwlknonel  27883  0pth  27913  frcond4  28058  1to3vfriswmgr  28068  3cyclfrgr  28076  frgrwopreglem5  28109  2clwwlk2clwwlk  28138  numclwlk1lem1  28157  numclwwlk6  28178  ajval  28647  issh  28994  dmadjss  29673  adjeu  29675  adjval  29676  isst  29999  ishst  30000  xrdifh  30532  nndiffz1  30538  xdivpnfrp  30638  isomnd  30755  isslmd  30883  isprmidl  31021  isprmidlc  31031  ismxidl  31042  isrrext  31349  ismntop  31375  isros  31535  issros  31542  issibf  31699  eulerpartleme  31729  eulerpartlemt0  31735  probun  31785  bnj250  32079  bnj255  32083  bnj345  32092  bnj945  32153  bnj1209  32176  bnj1275  32193  bnj543  32273  bnj571  32286  bnj607  32296  bnj882  32306  bnj983  32331  bnj996  32336  bnj1006  32340  bnj1033  32349  bnj1097  32361  bnj1110  32362  bnj1145  32373  bnj1174  32383  bnj1189  32389  bnj1450  32430  bnj1514  32443  cusgr3cyclex  32491  erdszelem1  32546  cvmsval  32621  cvmliftiota  32656  snmlval  32686  lediv2aALT  33028  elwlim  33218  nocvxminlem  33355  scutcut  33374  scutbday  33375  brtxp2  33450  brpprod3a  33455  brcart  33501  brsuccf  33510  broutsideof3  33695  ivthALT  33791  df3nandALT2  33856  andnand1  33857  topdifinffinlem  34759  relowlssretop  34775  rdgeqoa  34782  unccur  35033  fin2solem  35036  poimirlem3  35053  poimirlem4  35054  poimirlem26  35076  poimirlem27  35077  poimirlem32  35082  itg2gt0cn  35105  iblabsnclem  35113  areacirc  35143  neificl  35184  ablo4pnp  35311  isrngohom  35396  isidl  35445  ispridl  35465  pridlidl  35466  ismaxidl  35471  maxidlidl  35472  isfldidl2  35500  isdmn3  35505  triantru3  35653  moantr  35769  brxrn2  35780  dfxrn2  35781  ecxrn  35792  inxpxrn  35796  rnxrn  35799  islshp  36268  isopos  36469  cvrfval  36557  cvrval  36558  isatl  36588  isat3  36596  islpln5  36824  4atlem11  36898  dalem20  36982  lhpexle3  37301  lhpex2leN  37302  isltrn2N  37409  diclspsn  38483  lcfls1lem  38823  lcfls1N  38824  uzindd  39257  3cubes  39618  fz1eqin  39697  isdomn3  40135  rp-isfinite6  40213  snhesn  40474  ismnuprim  40989  iotasbc2  41111  eelT00  41398  eelTTT  41399  eelT11  41400  eelT12  41402  eelTT1  41403  eelT01  41404  eel0T1  41405  uun132  41478  uun132p1  41479  un2122  41483  uunTT1  41486  uunTT1p1  41487  uunTT1p2  41488  uunT11  41489  uunT11p1  41490  uunT11p2  41491  uunT12  41492  uunT12p1  41493  uunT12p2  41494  uunT12p3  41495  uunT12p4  41496  uunT12p5  41497  uun111  41498  uun2221  41506  uun2221p1  41507  uun2221p2  41508  stoweidlem17  42646  stoweidlem34  42663  stoweidlem60  42689  ndmaovass  43749  ndmaovdistr  43750  4an21  43813  2elfz3nn0  43860  prproropf1o  44011  fpprel  44233  upwlksfval  44350  isupwlkg  44352  upwlkbprop  44353  isrng  44487  2zrngnmrid  44561  lindslinindsimp2lem5  44858  elpg  45230  alimp-no-surprise  45296
  Copyright terms: Public domain W3C validator