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

Theorem 3anass 1109
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 1102 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 456 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 266 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3anan12  1110  3ancoma  1112  3anan12OLD  1116  3anrotOLD  1117  anandi3  1120  3biant1d  1595  an33rean  1600  cad1  1710  3exdistr  2050  ceqsex2  3449  ceqsex3v  3451  ceqsex4v  3452  ceqsex6v  3453  ceqsex8v  3454  2reu5lem1  3622  2reu5lem2  3623  2reu5lem3  3624  eldifpr  4409  rexdifpr  4410  trel3  4965  2rbropap  5223  ordelord  5969  dflim2  6004  dff1o4  6368  foco2  6608  brfvopab  6937  ndmovass  7059  ndmovdistr  7060  dflim3  7284  dflim4  7285  mpt2xopovel  7588  dfsmo2  7687  dfrecs3  7712  oeeui  7926  ecopovtrn  8093  elixp2  8156  elixp  8159  mptelixpg  8189  eqinf  8636  zorn2lem7  9616  grothprim  9948  grothtsk  9949  divmulasscom  11001  muldivdir  11012  divmuldiv  11017  sup3  11272  dfnn3  11326  prime  11731  eluz2  11917  raluz2  11962  elixx1  12409  elixx3g  12413  elioo2  12441  elioo5  12456  elicc4  12465  iccneg  12521  icoshft  12522  difreicc  12534  elfz1  12561  elfz  12562  elfz2  12563  elfzm11  12641  elfz2nn0  12661  elfzo2  12704  elfzo3  12717  lbfzo0  12739  fzind2  12817  zmodid2  12929  swrdnd2  13664  swrdccatin1  13714  swrdccat  13724  repswswrd  13762  swrdco  13814  2swrd2eqwrdeq  13928  ccat2s1fvwALT  13930  rediv  14101  imdiv  14108  cosmul  15130  bitsval  15372  bitsmod  15384  bitscmp  15386  smueqlem  15438  dfgcd2  15489  lcmneg  15542  lcmftp  15575  coprmgcdb  15588  divgcdcoprmex  15605  cncongr1  15606  cncongr2  15607  difsqpwdvds  15815  oddprmdvds  15831  elgz  15859  xpsfrnel  16435  xpsfrnel2  16437  ismre  16462  mreexexlem4d  16519  iscatd2  16553  isssc  16691  eldmcoa  16926  isdrs  17146  isipodrs  17373  ismhm  17549  mhmpropd  17553  issubm  17559  submacs  17577  issubg  17803  eqglact  17854  eqgid  17855  pgrpsubgsymgbi  18035  isslw  18231  efgsdm  18351  mulgmhm  18441  mulgghm  18442  dmdprd  18606  dprdw  18618  subgdmdprd  18642  dmdprdpr  18657  issrg  18716  srglmhm  18744  srgrmhm  18745  isring  18760  ringlghm  18813  dfrhm2  18928  issubrg3  19019  islmod  19078  lsspropd  19231  islmhm  19241  islbs  19290  lbspropd  19313  isphl  20190  elocv  20230  isobs  20282  mat1dimscm  20500  scmatghm  20558  scmatmhm  20559  ma1repvcl  20595  smadiadetr  20701  mat2pmatghm  20756  mat2pmatmul  20757  decpmatmulsumfsupp  20799  pm2mpghm  20842  pm2mpmhmlem1  20844  neindisj  21143  lmbrf  21286  hauscmplem  21431  llyi  21499  subislly  21506  islocfin  21542  uptx  21650  txcn  21651  qtopeu  21741  elmptrab  21852  isfbas  21854  trfil2  21912  flimcls  22010  cnextcn  22092  xmetec  22460  ngppropd  22662  ngpocelbl  22729  bl2ioo  22816  xrtgioo  22830  om1elbas  23052  elpi1  23065  isclm  23084  isclmp  23117  isncvsngp  23169  iscph  23190  tchcph  23256  lmmbr2  23278  lmmbrf  23281  iscau2  23296  caussi  23316  lmclim  23322  bcthlem1  23342  srabn  23377  ishl2  23387  evthicc2  23451  ovolfioo  23458  ovolficc  23459  iblcnlem1  23778  iblrelem  23781  iblre  23784  iblcn  23789  isuc1p  24124  ismon1p  24126  ellogrn  24530  logreclem  24724  atandm  24827  atandm2  24828  atandm3  24829  atans2  24882  dmarea  24908  dchrelbas4  25192  lgsmodeq  25291  lgsmulsqcoprm  25292  ax5seg  26042  eengtrkg  26089  uspgredg2v  26341  nbgrelOLD  26460  nb3grpr2  26511  isrusgr0  26700  rusgrprop0  26701  ewlkprop  26737  wksfval  26743  wlkeq  26767  wlkson  26790  wlkonprop  26792  upgr2wlk  26802  upgrtrls  26836  upgristrl  26837  wksonproplem  26839  pthsfval  26855  ispth  26857  isspthonpth  26883  uhgrwkspth  26889  usgr2wlkspth  26893  crctcshwlkn0lem4  26944  wspthnp  26982  wwlknon  26991  wwlknonOLD  26993  wwlksnextwrd  27044  wwlksnextinj  27046  wspthsnwspthsnon  27064  wspthsnwspthsnonOLD  27066  umgr2adedgwlk  27095  umgr2adedgwlkon  27096  umgr2adedgwlkonALT  27097  umgr2adedgspth  27098  s3wwlks2on  27107  wpthswwlks2on  27112  wpthswwlks2onOLD  27113  usgr2wspthons3  27116  usgr2wspthon  27117  elwwlks2  27118  elwspths2spth  27119  rusgrnumwwlkl1  27120  rusgrnumwwlkslem  27121  isclwwlk  27137  clwwlkbp  27138  clwlkclwwlklem3  27154  isclwwlknx  27194  clwwlknp  27195  clwwlkn1  27200  clwwlkn2  27203  clwwlkwwlksb  27214  clwlksfclwwlkOLD  27246  clwwlknonel  27272  0pth  27308  frcond4  27455  1to3vfriswmgr  27465  3cyclfrgr  27473  frgrwopreglem5  27506  2clwwlk2clwwlk  27537  numclwwlkovgelOLD  27539  numclwlk1lem1  27559  numclwwlk6  27588  ajval  28055  issh  28403  dmadjss  29084  adjeu  29086  adjval  29087  isst  29410  ishst  29411  xrdifh  29879  nndiffz1  29885  xdivpnfrp  29976  isomnd  30036  isslmd  30090  isrrext  30379  ismntop  30405  isros  30566  issros  30573  issibf  30730  eulerpartleme  30760  eulerpartlemt0  30766  probun  30816  bnj250  31102  bnj255  31106  bnj345  31115  bnj945  31176  bnj1209  31199  bnj1275  31216  bnj543  31295  bnj571  31308  bnj607  31318  bnj882  31328  bnj983  31353  bnj996  31357  bnj1006  31361  bnj1033  31369  bnj1097  31381  bnj1110  31382  bnj1145  31393  bnj1174  31403  bnj1189  31409  bnj1450  31450  bnj1514  31463  erdszelem1  31505  cvmsval  31580  cvmliftiota  31615  snmlval  31645  lediv2aALT  31902  elwlim  32098  nocvxminlem  32223  scutcut  32242  scutbday  32243  brtxp2  32318  brpprod3a  32323  brcart  32369  brsuccf  32378  broutsideof3  32563  ivthALT  32660  df3nandALT2  32725  andnand1  32726  topdifinffinlem  33517  relowlssretop  33533  rdgeqoa  33540  unccur  33711  fin2solem  33714  poimirlem3  33731  poimirlem4  33732  poimirlem26  33754  poimirlem27  33755  poimirlem32  33760  itg2gt0cn  33783  iblabsnclem  33791  areacirc  33823  neificl  33866  ablo4pnp  33996  isrngohom  34081  isidl  34130  ispridl  34150  pridlidl  34151  ismaxidl  34156  maxidlidl  34157  isfldidl2  34185  isdmn3  34190  triantru3  34327  eldmqsres  34374  moantr  34446  brxrn2  34456  dfxrn2  34457  ecxrn  34468  xrninxp2  34470  inxpxrn  34472  rnxrn  34475  islshp  34765  isopos  34966  cvrfval  35054  cvrval  35055  isatl  35085  isat3  35093  islpln5  35321  4atlem11  35395  dalem20  35479  lhpexle3  35798  lhpex2leN  35799  isltrn2N  35906  diclspsn  36980  lcfls1lem  37320  lcfls1N  37321  fz1eqin  37839  issdrg  38273  sdrgacs  38277  isdomn3  38288  rp-isfinite6  38369  snhesn  38585  iotasbc2  39125  eelT00  39433  eelTTT  39434  eelT11  39435  eelT12  39437  eelTT1  39438  eelT01  39439  eel0T1  39440  uun132  39514  uun132p1  39515  un2122  39519  uunTT1  39522  uunTT1p1  39523  uunTT1p2  39524  uunT11  39525  uunT11p1  39526  uunT11p2  39527  uunT12  39528  uunT12p1  39529  uunT12p2  39530  uunT12p3  39531  uunT12p4  39532  uunT12p5  39533  uun111  39534  uun2221  39542  uun2221p1  39543  uun2221p2  39544  stoweidlem17  40718  stoweidlem34  40735  stoweidlem60  40761  ndmaovass  41800  ndmaovdistr  41801  4an21  41864  2elfz3nn0  41906  reuccatpfxs1  42014  upwlksfval  42289  isupwlkg  42291  upwlkbprop  42292  isrng  42449  2zrngnmrid  42523  lindslinindsimp2lem5  42824  elpg  43033  alimp-no-surprise  43103
  Copyright terms: Public domain W3C validator