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

Theorem 3anass 1059
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 1056 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 682 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  3anrot  1060  3anan12  1069  anandi3  1070  3biant1d  1481  an33rean  1486  cad1  1595  3exdistr  1926  ceqsex2  3275  ceqsex3v  3277  ceqsex4v  3278  ceqsex6v  3279  ceqsex8v  3280  2reu5lem1  3446  2reu5lem2  3447  2reu5lem3  3448  eldifpr  4237  rexdifpr  4238  trel3  4793  2rbropap  5046  ordelord  5783  dflim2  5819  dff1o4  6183  foco2  6419  brfvopab  6742  ndmovass  6864  ndmovdistr  6865  dflim3  7089  dflim4  7090  mpt2xopovel  7391  dfsmo2  7489  dfrecs3  7514  oeeui  7727  ecopovtrn  7893  elixp2  7954  elixp  7957  mptelixpg  7987  eqinf  8431  zorn2lem7  9362  grothprim  9694  grothtsk  9695  divmulasscom  10747  muldivdir  10758  divmuldiv  10763  sup3  11018  dfnn3  11072  prime  11496  eluz2  11731  raluz2  11775  elixx1  12222  elixx3g  12226  elioo2  12254  elioo5  12269  elicc4  12278  iccneg  12331  icoshft  12332  difreicc  12342  elfz1  12369  elfz  12370  elfz2  12371  elfzm11  12449  elfz2nn0  12469  elfzo2  12512  elfzo3  12525  lbfzo0  12547  fzind2  12626  zmodid2  12738  swrdnd2  13479  swrdccatin1  13529  swrdccat  13539  repswswrd  13577  swrdco  13629  2swrd2eqwrdeq  13742  ccat2s1fvwALT  13744  rediv  13915  imdiv  13922  cosmul  14947  bitsval  15193  bitsmod  15205  bitscmp  15207  smueqlem  15259  dfgcd2  15310  lcmneg  15363  lcmftp  15396  coprmgcdb  15409  divgcdcoprmex  15427  cncongr1  15428  cncongr2  15429  difsqpwdvds  15638  oddprmdvds  15654  elgz  15682  xpsfrnel  16270  xpsfrnel2  16272  ismre  16297  mreexexlem4d  16354  iscatd2  16389  isssc  16527  eldmcoa  16762  isdrs  16981  isipodrs  17208  ismhm  17384  mhmpropd  17388  issubm  17394  submacs  17412  issubg  17641  eqglact  17692  eqgid  17693  pgrpsubgsymgbi  17873  isslw  18069  efgsdm  18189  mulgmhm  18279  mulgghm  18280  dmdprd  18443  dprdw  18455  subgdmdprd  18479  dmdprdpr  18494  issrg  18553  srglmhm  18581  srgrmhm  18582  isring  18597  ringlghm  18650  dfrhm2  18765  issubrg3  18856  islmod  18915  lsspropd  19065  islmhm  19075  islbs  19124  lbspropd  19147  isphl  20021  elocv  20060  isobs  20112  mat1dimscm  20329  scmatghm  20387  scmatmhm  20388  ma1repvcl  20424  smadiadetr  20529  mat2pmatghm  20583  mat2pmatmul  20584  decpmatmulsumfsupp  20626  pm2mpghm  20669  pm2mpmhmlem1  20671  neindisj  20969  lmbrf  21112  hauscmplem  21257  llyi  21325  subislly  21332  islocfin  21368  uptx  21476  txcn  21477  qtopeu  21567  elmptrab  21678  isfbas  21680  trfil2  21738  flimcls  21836  cnextcn  21918  xmetec  22286  ngppropd  22488  ngpocelbl  22555  bl2ioo  22642  xrtgioo  22656  om1elbas  22878  elpi1  22891  isclm  22910  isclmp  22943  isncvsngp  22995  iscph  23016  tchcph  23082  lmmbr2  23103  lmmbrf  23106  iscau2  23121  caussi  23141  lmclim  23147  bcthlem1  23167  srabn  23202  ishl2  23212  evthicc2  23275  ovolfioo  23282  ovolficc  23283  iblcnlem1  23599  iblrelem  23602  iblre  23605  iblcn  23610  isuc1p  23945  ismon1p  23947  ellogrn  24351  logreclem  24545  atandm  24648  atandm2  24649  atandm3  24650  atans2  24703  dmarea  24729  dchrelbas4  25013  lgsmodeq  25112  lgsmulsqcoprm  25113  ax5seg  25863  eengtrkg  25910  uspgredg2v  26161  nbgrelOLD  26279  nb3grpr2  26329  isrusgr0  26518  rusgrprop0  26519  ewlkprop  26555  wksfval  26561  wlkeq  26585  wlkson  26608  wlkonprop  26610  upgr2wlk  26620  upgrtrls  26654  upgristrl  26655  wksonproplem  26657  pthsfval  26673  ispth  26675  isspthonpth  26701  uhgrwkspth  26707  usgr2wlkspth  26711  crctcshwlkn0lem4  26761  wspthnp  26799  wwlknon  26808  wwlknonOLD  26810  wwlksnextwrd  26860  wwlksnextinj  26862  wspthsnwspthsnon  26879  wspthsnwspthsnonOLD  26881  umgr2adedgwlk  26910  umgr2adedgwlkon  26911  umgr2adedgwlkonALT  26912  umgr2adedgspth  26913  s3wwlks2on  26922  wpthswwlks2on  26927  wpthswwlks2onOLD  26928  usgr2wspthons3  26931  usgr2wspthon  26932  elwwlks2  26933  elwspths2spth  26934  rusgrnumwwlkl1  26935  rusgrnumwwlkslem  26936  isclwwlk  26952  clwwlkbp  26953  clwlkclwwlklem3  26967  isclwwlknx  26998  clwwlknp  26999  clwwlkn1  27004  clwwlkn2  27007  clwwlkwwlksb  27018  clwlksfclwwlk  27049  clwwlknonel  27070  0pth  27103  frcond4  27250  1to3vfriswmgr  27260  3cyclfrgr  27268  frgrwopreglem5  27301  numclwwlkovgelOLD  27340  numclwwlk6  27377  ajval  27845  issh  28193  dmadjss  28874  adjeu  28876  adjval  28877  isst  29200  ishst  29201  xrdifh  29670  nndiffz1  29676  xdivpnfrp  29769  isomnd  29829  isslmd  29883  isrrext  30172  ismntop  30198  isros  30359  issros  30366  issibf  30523  eulerpartleme  30553  eulerpartlemt0  30559  probun  30609  bnj250  30895  bnj255  30899  bnj345  30908  bnj945  30970  bnj1209  30993  bnj1275  31010  bnj543  31089  bnj571  31102  bnj607  31112  bnj882  31122  bnj983  31147  bnj996  31151  bnj1006  31155  bnj1033  31163  bnj1097  31175  bnj1110  31176  bnj1145  31187  bnj1174  31197  bnj1189  31203  bnj1450  31244  bnj1514  31257  erdszelem1  31299  cvmsval  31374  cvmliftiota  31409  snmlval  31439  lediv2aALT  31697  elwlim  31893  nocvxminlem  32018  scutcut  32037  scutbday  32038  brtxp2  32113  brpprod3a  32118  brcart  32164  brsuccf  32173  broutsideof3  32358  ivthALT  32455  df3nandALT2  32522  andnand1  32523  topdifinffinlem  33325  relowlssretop  33341  rdgeqoa  33348  unccur  33522  fin2solem  33525  poimirlem3  33542  poimirlem4  33543  poimirlem26  33565  poimirlem27  33566  poimirlem32  33571  itg2gt0cn  33595  iblabsnclem  33603  areacirc  33635  neificl  33679  ablo4pnp  33809  isrngohom  33894  isidl  33943  ispridl  33963  pridlidl  33964  ismaxidl  33969  maxidlidl  33970  isfldidl2  33998  isdmn3  34003  triantru3  34143  eldmqsres  34192  moantr  34267  brxrn2  34277  dfxrn2  34278  ecxrn  34289  xrninxp2  34291  inxpxrn  34293  rnxrn  34296  islshp  34584  isopos  34785  cvrfval  34873  cvrval  34874  isatl  34904  isat3  34912  islpln5  35139  4atlem11  35213  dalem20  35297  lhpexle3  35616  lhpex2leN  35617  isltrn2N  35724  diclspsn  36800  lcfls1lem  37140  lcfls1N  37141  fz1eqin  37649  issdrg  38084  sdrgacs  38088  isdomn3  38099  rp-isfinite6  38181  snhesn  38397  iotasbc2  38938  eelT00  39247  eelTTT  39248  eelT11  39249  eelT12  39251  eelTT1  39252  eelT01  39253  eel0T1  39254  uun132  39329  uun132p1  39330  un2122  39334  uunTT1  39337  uunTT1p1  39338  uunTT1p2  39339  uunT11  39340  uunT11p1  39341  uunT11p2  39342  uunT12  39343  uunT12p1  39344  uunT12p2  39345  uunT12p3  39346  uunT12p4  39347  uunT12p5  39348  uun111  39349  uun2221  39357  uun2221p1  39358  uun2221p2  39359  stoweidlem17  40552  stoweidlem34  40569  stoweidlem60  40595  ndmaovass  41607  ndmaovdistr  41608  4an21  41611  2elfz3nn0  41651  reuccatpfxs1  41759  upwlksfval  42041  isupwlkg  42043  upwlkbprop  42044  isrng  42201  2zrngnmrid  42275  lindslinindsimp2lem5  42576  elpg  42785  alimp-no-surprise  42855
  Copyright terms: Public domain W3C validator