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

Theorem anass 469
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 468 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 467 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 210 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  bianass  638  an31  644  an4  652  3anass  1087  3an4anass  1097  2sb5  2274  r19.41v  3347  r19.41  3348  rabrab  3380  ceqsex3v  3546  spc2ed  3601  ceqsrex2v  3650  rexrab  3686  rexrab2  3692  2reu5  3748  rexss  4037  inass  4195  rexin  4215  indifdir  4259  difin2  4265  difrab  4276  reupick3  4287  inssdif0  4328  rexdifpr  4590  rexdifsn  4721  reusv2lem4  5293  reusv2  5295  eqvinop  5370  copsexgw  5373  copsexg  5374  rabxp  5594  elvvv  5621  resopab2  5898  difxp  6015  mptpreima  6086  resco  6097  coass  6112  wfi  6175  imadif  6432  dff1o2  6614  eqfnfv3  6797  f1ossf1o  6883  isoini  7080  f1oiso  7093  oprabidw  7176  oprabid  7177  dfoprab2  7201  mpoeq123  7215  mpomptx  7254  resoprab2  7260  ov3  7300  uniuni  7472  elxp4  7615  elxp5  7616  oprabex3  7669  frxp  7811  rexsupp  7839  brtpos2  7889  oeeui  8218  oeeu  8219  omabs  8264  mapsnend  8577  xpsnen  8590  xpcomco  8596  xpassen  8600  wemapsolem  9003  epfrs  9162  aceq1  9532  dfac5lem1  9538  dfac5lem2  9539  dfac5lem5  9542  kmlem3  9567  kmlem14  9578  pwfseqlem1  10069  ltexpi  10313  ltexprlem4  10450  axaddf  10556  axmulf  10557  rexuz  12287  rexuz2  12288  nnwos  12304  zmin  12333  rexrp  12400  elixx3g  12741  elfz2  12889  preduz  13019  fzind2  13145  hashbclem  13800  resqrex  14600  rlim  14842  divalglem10  15743  divalgb  15745  gcdass  15885  lcmass  15948  isprm2  16016  infpn2  16239  ispos2  17548  issubmndb  17960  issubg3  18237  resscntz  18402  subgdmdprd  19087  dprd2d2  19097  dfrhm2  19400  isassa  20018  aspval2  20057  fvmptnn04if  21387  ntreq0  21615  cmpcov2  21928  llyi  22012  nllyi  22013  ptpjpre1  22109  tx1cn  22147  tx2cn  22148  txtube  22178  txkgen  22190  trfil2  22425  elflim2  22502  cnpflfi  22537  isfcls  22547  cnextcn  22605  istlm  22722  blres  22970  metrest  23063  isnlm  23213  elpi1  23578  isclmp  23630  iscvsp  23661  isncvsngp  23682  iscph  23703  cfilucfil3  23852  itg1climres  24244  itgsubst  24575  ulmdvlem3  24919  cubic  25354  vmasum  25720  lgsquadlem1  25884  lgsquadlem2  25885  legov  26299  perpln1  26424  axcontlem5  26682  nbgrel  27050  nbusgredgeu0  27078  nb3grpr2  27093  finsumvtxdg2ssteplem3  27257  usgr2pth0  27474  isclwlke  27486  wwlksnfi  27612  wwlksnfiOLD  27613  elwwlks2ons3  27662  wpthswwlks2on  27668  usgr2wspthon  27672  rusgrnumwwlkl1  27675  isclwwlk  27690  isclwwlknx  27742  clwlknf1oclwwlkn  27791  clwwlknonel  27802  clwwlknon2x  27810  clwwlkvbij  27820  iseupthf1o  27909  fusgr2wsp2nb  28041  grpoidinvlem3  28211  h2hlm  28685  issh  28913  issh3  28924  ocsh  28988  cvbr2  29988  cvnbtwn2  29992  mdsl2i  30027  cvmdi  30029  mdsymlem2  30109  sumdmdii  30120  dmrab  30188  difrab2  30189  disjunsn  30273  mpomptxf  30354  1stpreima  30369  2ndpreima  30370  f1od2  30384  nndiffz1  30436  omndmul2  30641  smatrcl  30961  crefdf  31012  1stmbfm  31418  2ndmbfm  31419  dya2iocnei  31440  eulerpartlemgvv  31534  eulerpartlemn  31539  bnj250  31871  bnj251  31872  bnj256  31876  bnj168  31900  cusgr3cyclex  32281  iscvm  32404  axacprim  32831  dfpo2  32889  dfdm5  32914  dfrn5  32915  elima4  32917  frpoind  32978  frind  32983  sltval2  33061  madeval2  33188  dfon3  33251  brimg  33296  dfrecs2  33309  dfrdg4  33310  ifscgr  33403  cgrxfr  33414  segcon2  33464  seglecgr12im  33469  segletr  33473  ellines  33511  neifg  33617  bj-dfmpoa  34303  bj-imdirid  34368  topdifinffinlem  34511  icorempo  34515  difunieq  34538  finxpreclem6  34560  wl-cases2-dnf  34635  curf  34752  uncf  34753  matunitlindflem2  34771  matunitlindf  34772  poimirlem26  34800  poimirlem28  34802  poimirlem30  34804  poimirlem32  34806  poimir  34807  itg2addnc  34828  ftc1anclem5  34853  ftc1anc  34857  areacirclem5  34868  isbnd2  34944  heibor1  34971  anan  35382  inxpxrn  35525  prtlem70  35875  prtlem100  35877  lsateln0  36013  islshpat  36035  lcvbr2  36040  lcvnbtwn2  36045  isopos  36198  cvrval2  36292  cvrnbtwn2  36293  ishlat2  36371  3dim0  36475  islvol5  36597  pmapjat1  36871  pclcmpatN  36919  pclfinclN  36968  cdlemefrs29pre00  37413  cdlemefrs29bpre0  37414  cdlemefrs29cpre1  37416  cdleme32a  37459  cdlemftr3  37583  dvhopellsm  38135  dibelval3  38165  diblsmopel  38189  mapdvalc  38647  mapdval4N  38650  mapdordlem1a  38652  diophrex  39252  rmxdioph  39493  dford4  39506  islmodfg  39549  islssfg2  39551  isdomn3  39684  fgraphopab  39690  k0004lem1  40377  ismnuprim  40510  2sbc5g  40628  limcrecl  41790  dvnmul  42108  dvnprodlem2  42112  fourierdlem83  42355  iundjiun  42623  4an21  43350  sprvalpwn0  43492  pairreueq  43519  prprsprreu  43528  prprreueq  43529  isrnghm  44061  isrnghmmul  44062  rngcinv  44150  rngcinvALTV  44162  ringcinv  44201  ringcinvALTV  44225  mpomptx2  44281
  Copyright terms: Public domain W3C validator