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

Theorem anass 679
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
anass (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))

Proof of Theorem anass
StepHypRef Expression
1 id 22 . . 3 ((𝜑 ∧ (𝜓𝜒)) → (𝜑 ∧ (𝜓𝜒)))
21anassrs 678 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 677 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 198 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  an12  834  an32  835  an13  836  an31  837  bianass  838  an4  861  3anass  1035  3an4anass  1283  2sb5  2431  r19.41v  3070  r19.41  3071  ceqsex3v  3219  ceqsrex2v  3308  rexrab  3337  rexrab2  3341  2reu5  3383  rexss  3632  inass  3785  indifdir  3842  difin2  3849  difrab  3860  reupick3  3871  inssdif0  3901  rexdifsn  4264  reusv2lem4  4798  reusv2  4800  eqvinop  4881  copsexg  4882  wefrc  5032  rabxp  5078  elvvv  5101  resopab2  5368  difxp  5477  ssrnres  5491  mptpreima  5545  coass  5571  wfi  5630  imadif  5887  dff1o2  6055  eqfnfv3  6221  isoini  6488  f1oiso  6501  oprabid  6576  dfoprab2  6599  mpt2eq123  6612  mpt2mptx  6649  resoprab2  6655  ov3  6695  uniuni  6865  elxp4  7003  elxp5  7004  oprabex3  7048  frxp  7174  rexsupp  7200  brtpos2  7245  oeeui  7569  oeeu  7570  omabs  7614  mapsnen  7920  xpsnen  7929  xpcomco  7935  xpassen  7939  wemapsolem  8338  epfrs  8490  bnd2  8639  aceq1  8823  dfac5lem1  8829  dfac5lem2  8830  dfac5lem5  8833  kmlem3  8857  kmlem14  8868  pwfseqlem1  9359  ltexpi  9603  ltexprlem4  9740  axaddf  9845  axmulf  9846  rexuz  11614  rexuz2  11615  nnwos  11631  zmin  11660  rexrp  11729  elixx3g  12059  elfz2  12204  preduz  12330  fzind2  12448  hashbclem  13093  resqrex  13839  rlim  14074  divalglem10  14963  divalgb  14965  gcdass  15102  lcmass  15165  isprm2  15233  infpn2  15455  ispos2  16771  issubg3  17435  resscntz  17587  subgdmdprd  18256  dprd2d2  18266  dfrhm2  18540  isassa  19136  aspval2  19168  fvmptnn04if  20473  ntreq0  20691  cmpcov2  21003  llyi  21087  nllyi  21088  subislly  21094  ptpjpre1  21184  tx1cn  21222  tx2cn  21223  txtube  21253  txkgen  21265  trfil2  21501  elflim2  21578  cnpflfi  21613  isfcls  21623  cnextcn  21681  istlm  21798  blres  22046  metrest  22139  isnlm  22289  elcncf1di  22506  elpi1  22653  isclmp  22705  iscvsp  22736  isncvsngp  22757  iscph  22778  cfilucfil3  22925  itg1climres  23287  itgsubst  23616  ulmdvlem3  23960  cubic  24376  vmasum  24741  logfac2  24742  lgsquadlem1  24905  lgsquadlem2  24906  legov  25280  ltgov  25292  perpln1  25405  axcontlem5  25648  nb3grapr2  25983  trls  26066  3v3e3cycl2  26192  wwlknprop  26214  wwlkextwrd  26256  wwlknfi  26266  wlknwwlknvbij  26268  isclwlk  26284  clwwlkvbij  26329  usg2spthonot0  26416  usg2spthonot1  26417  rusgranumwlkl1  26474  rusgranumwlklem3  26478  rusgra0edg  26482  1to2vfriswmgra  26533  usgreg2spot  26594  numclwwlkovf2  26611  grpoidinvlem3  26744  h2hlm  27221  issh  27449  issh3  27460  ocsh  27526  cvbr2  28526  cvnbtwn2  28530  mdsl2i  28565  cvmdi  28567  mdsymlem2  28647  sumdmdii  28658  spc2ed  28696  rabrab  28722  disjunsn  28789  mpt2mptxf  28860  1stpreima  28867  2ndpreima  28868  f1od2  28887  nndiffz1  28936  omndmul2  29043  smatrcl  29190  crefdf  29243  pcmplfin  29255  1stmbfm  29649  2ndmbfm  29650  dya2iocnei  29671  eulerpartlemgvv  29765  eulerpartlemn  29770  bnj250  30020  bnj251  30021  bnj256  30025  bnj168  30052  iscvm  30495  axacprim  30838  dfpo2  30898  dfdm5  30921  dfrn5  30922  elima4  30924  frind  30984  sltval2  31053  nofulllem5  31105  dfon3  31169  brimg  31214  dfrecs2  31227  dfrdg4  31228  ifscgr  31321  cgrxfr  31332  segcon2  31382  seglecgr12im  31387  segletr  31391  ellines  31429  neifg  31536  bj-dfmpt2a  32252  topdifinffinlem  32371  icorempt2  32375  finxpreclem6  32409  wl-cases2-dnf  32474  curf  32557  uncf  32558  matunitlindflem2  32576  matunitlindf  32577  poimirlem26  32605  poimirlem28  32607  poimirlem30  32609  poimirlem32  32611  poimir  32612  itg2addnc  32634  ftc1anclem5  32659  ftc1anc  32663  areacirclem5  32674  isbnd2  32752  heibor1  32779  prtlem70  33157  prtlem100  33161  lsateln0  33300  islshpat  33322  lcvbr2  33327  lcvnbtwn2  33332  isopos  33485  cvrval2  33579  cvrnbtwn2  33580  ishlat2  33658  3dim0  33761  islvol5  33883  pmapjat1  34157  pclcmpatN  34205  pclfinclN  34254  cdlemefrs29pre00  34701  cdlemefrs29bpre0  34702  cdlemefrs29cpre1  34704  cdleme32a  34747  cdlemftr3  34871  dvhopellsm  35424  dibelval3  35454  diblsmopel  35478  mapdvalc  35936  mapdval4N  35939  mapdordlem1a  35941  diophrex  36357  rmxdioph  36601  dford4  36614  islmodfg  36657  islssfg2  36659  isdomn3  36801  fgraphopab  36807  k0004lem1  37465  2sbc5g  37639  mapsnend  38386  limcrecl  38696  dvnmul  38833  dvnprodlem2  38837  fourierdlem83  39082  iundjiun  39353  rexdifpr  40315  nbgrel  40564  nbusgredgeu0  40596  nb3grpr2  40611  usgr2pth0  40971  isclWlke  40984  wwlksnfi  41112  wlksnwwlknvbij  41114  elwwlks2ons3  41159  wpthswwlks2on  41164  usgr2wspthon  41168  rusgrnumwwlkl1  41172  isclwwlks  41188  isclwwlksnx  41197  clwwlksvbij  41229  iseupthf1o  41369  av-numclwwlkovf2  41515  isrnghm  41682  isrnghmmul  41683  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  mpt2mptx2  41906
  Copyright terms: Public domain W3C validator