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

Theorem 3anass 1081
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 1074 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 684 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1072
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 1074
This theorem is referenced by:  3anan12  1082  3ancoma  1084  3anan12OLD  1088  3anrotOLD  1089  anandi3  1092  3biant1d  1590  an33rean  1595  cad1  1704  3exdistr  2035  ceqsex2  3384  ceqsex3v  3386  ceqsex4v  3387  ceqsex6v  3388  ceqsex8v  3389  2reu5lem1  3554  2reu5lem2  3555  2reu5lem3  3556  eldifpr  4349  rexdifpr  4350  trel3  4912  2rbropap  5167  ordelord  5906  dflim2  5942  dff1o4  6306  foco2  6542  brfvopab  6865  ndmovass  6987  ndmovdistr  6988  dflim3  7212  dflim4  7213  mpt2xopovel  7515  dfsmo2  7613  dfrecs3  7638  oeeui  7851  ecopovtrn  8017  elixp2  8078  elixp  8081  mptelixpg  8111  eqinf  8555  zorn2lem7  9516  grothprim  9848  grothtsk  9849  divmulasscom  10901  muldivdir  10912  divmuldiv  10917  sup3  11172  dfnn3  11226  prime  11650  eluz2  11885  raluz2  11930  elixx1  12377  elixx3g  12381  elioo2  12409  elioo5  12424  elicc4  12433  iccneg  12486  icoshft  12487  difreicc  12497  elfz1  12524  elfz  12525  elfz2  12526  elfzm11  12604  elfz2nn0  12624  elfzo2  12667  elfzo3  12680  lbfzo0  12702  fzind2  12780  zmodid2  12892  swrdnd2  13633  swrdccatin1  13683  swrdccat  13693  repswswrd  13731  swrdco  13783  2swrd2eqwrdeq  13897  ccat2s1fvwALT  13899  rediv  14070  imdiv  14077  cosmul  15102  bitsval  15348  bitsmod  15360  bitscmp  15362  smueqlem  15414  dfgcd2  15465  lcmneg  15518  lcmftp  15551  coprmgcdb  15564  divgcdcoprmex  15582  cncongr1  15583  cncongr2  15584  difsqpwdvds  15793  oddprmdvds  15809  elgz  15837  xpsfrnel  16425  xpsfrnel2  16427  ismre  16452  mreexexlem4d  16509  iscatd2  16543  isssc  16681  eldmcoa  16916  isdrs  17135  isipodrs  17362  ismhm  17538  mhmpropd  17542  issubm  17548  submacs  17566  issubg  17795  eqglact  17846  eqgid  17847  pgrpsubgsymgbi  18027  isslw  18223  efgsdm  18343  mulgmhm  18433  mulgghm  18434  dmdprd  18597  dprdw  18609  subgdmdprd  18633  dmdprdpr  18648  issrg  18707  srglmhm  18735  srgrmhm  18736  isring  18751  ringlghm  18804  dfrhm2  18919  issubrg3  19010  islmod  19069  lsspropd  19219  islmhm  19229  islbs  19278  lbspropd  19301  isphl  20175  elocv  20214  isobs  20266  mat1dimscm  20483  scmatghm  20541  scmatmhm  20542  ma1repvcl  20578  smadiadetr  20683  mat2pmatghm  20737  mat2pmatmul  20738  decpmatmulsumfsupp  20780  pm2mpghm  20823  pm2mpmhmlem1  20825  neindisj  21123  lmbrf  21266  hauscmplem  21411  llyi  21479  subislly  21486  islocfin  21522  uptx  21630  txcn  21631  qtopeu  21721  elmptrab  21832  isfbas  21834  trfil2  21892  flimcls  21990  cnextcn  22072  xmetec  22440  ngppropd  22642  ngpocelbl  22709  bl2ioo  22796  xrtgioo  22810  om1elbas  23032  elpi1  23045  isclm  23064  isclmp  23097  isncvsngp  23149  iscph  23170  tchcph  23236  lmmbr2  23257  lmmbrf  23260  iscau2  23275  caussi  23295  lmclim  23301  bcthlem1  23321  srabn  23356  ishl2  23366  evthicc2  23429  ovolfioo  23436  ovolficc  23437  iblcnlem1  23753  iblrelem  23756  iblre  23759  iblcn  23764  isuc1p  24099  ismon1p  24101  ellogrn  24505  logreclem  24699  atandm  24802  atandm2  24803  atandm3  24804  atans2  24857  dmarea  24883  dchrelbas4  25167  lgsmodeq  25266  lgsmulsqcoprm  25267  ax5seg  26017  eengtrkg  26064  uspgredg2v  26315  nbgrelOLD  26433  nb3grpr2  26483  isrusgr0  26672  rusgrprop0  26673  ewlkprop  26709  wksfval  26715  wlkeq  26739  wlkson  26762  wlkonprop  26764  upgr2wlk  26774  upgrtrls  26808  upgristrl  26809  wksonproplem  26811  pthsfval  26827  ispth  26829  isspthonpth  26855  uhgrwkspth  26861  usgr2wlkspth  26865  crctcshwlkn0lem4  26916  wspthnp  26954  wwlknon  26963  wwlknonOLD  26965  wwlksnextwrd  27015  wwlksnextinj  27017  wspthsnwspthsnon  27034  wspthsnwspthsnonOLD  27036  umgr2adedgwlk  27065  umgr2adedgwlkon  27066  umgr2adedgwlkonALT  27067  umgr2adedgspth  27068  s3wwlks2on  27077  wpthswwlks2on  27082  wpthswwlks2onOLD  27083  usgr2wspthons3  27086  usgr2wspthon  27087  elwwlks2  27088  elwspths2spth  27089  rusgrnumwwlkl1  27090  rusgrnumwwlkslem  27091  isclwwlk  27107  clwwlkbp  27108  clwlkclwwlklem3  27124  isclwwlknx  27164  clwwlknp  27165  clwwlkn1  27170  clwwlkn2  27173  clwwlkwwlksb  27184  clwlksfclwwlkOLD  27216  clwwlknonel  27242  0pth  27277  frcond4  27424  1to3vfriswmgr  27434  3cyclfrgr  27442  frgrwopreglem5  27475  2clwwlk2clwwlk  27507  numclwwlkovgelOLD  27509  numclwlk1lem1  27530  numclwwlk6  27558  ajval  28026  issh  28374  dmadjss  29055  adjeu  29057  adjval  29058  isst  29381  ishst  29382  xrdifh  29851  nndiffz1  29857  xdivpnfrp  29950  isomnd  30010  isslmd  30064  isrrext  30353  ismntop  30379  isros  30540  issros  30547  issibf  30704  eulerpartleme  30734  eulerpartlemt0  30740  probun  30790  bnj250  31076  bnj255  31080  bnj345  31089  bnj945  31151  bnj1209  31174  bnj1275  31191  bnj543  31270  bnj571  31283  bnj607  31293  bnj882  31303  bnj983  31328  bnj996  31332  bnj1006  31336  bnj1033  31344  bnj1097  31356  bnj1110  31357  bnj1145  31368  bnj1174  31378  bnj1189  31384  bnj1450  31425  bnj1514  31438  erdszelem1  31480  cvmsval  31555  cvmliftiota  31590  snmlval  31620  lediv2aALT  31878  elwlim  32074  nocvxminlem  32199  scutcut  32218  scutbday  32219  brtxp2  32294  brpprod3a  32299  brcart  32345  brsuccf  32354  broutsideof3  32539  ivthALT  32636  df3nandALT2  32703  andnand1  32704  topdifinffinlem  33506  relowlssretop  33522  rdgeqoa  33529  unccur  33705  fin2solem  33708  poimirlem3  33725  poimirlem4  33726  poimirlem26  33748  poimirlem27  33749  poimirlem32  33754  itg2gt0cn  33778  iblabsnclem  33786  areacirc  33818  neificl  33862  ablo4pnp  33992  isrngohom  34077  isidl  34126  ispridl  34146  pridlidl  34147  ismaxidl  34152  maxidlidl  34153  isfldidl2  34181  isdmn3  34186  triantru3  34326  eldmqsres  34375  moantr  34450  brxrn2  34460  dfxrn2  34461  ecxrn  34472  xrninxp2  34474  inxpxrn  34476  rnxrn  34479  islshp  34769  isopos  34970  cvrfval  35058  cvrval  35059  isatl  35089  isat3  35097  islpln5  35324  4atlem11  35398  dalem20  35482  lhpexle3  35801  lhpex2leN  35802  isltrn2N  35909  diclspsn  36985  lcfls1lem  37325  lcfls1N  37326  fz1eqin  37834  issdrg  38269  sdrgacs  38273  isdomn3  38284  rp-isfinite6  38366  snhesn  38582  iotasbc2  39123  eelT00  39432  eelTTT  39433  eelT11  39434  eelT12  39436  eelTT1  39437  eelT01  39438  eel0T1  39439  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  40737  stoweidlem34  40754  stoweidlem60  40780  ndmaovass  41792  ndmaovdistr  41793  4an21  41796  2elfz3nn0  41836  reuccatpfxs1  41944  upwlksfval  42226  isupwlkg  42228  upwlkbprop  42229  isrng  42386  2zrngnmrid  42460  lindslinindsimp2lem5  42761  elpg  42970  alimp-no-surprise  43040
  Copyright terms: Public domain W3C validator