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

Theorem anass 459
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 458 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 457 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 199 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382
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 383
This theorem is referenced by:  bianass  623  an12  624  an32  625  an13  626  an31  627  an4  635  3anass  1080  3an4anass  1093  2sb5  2276  r19.41v  3237  r19.41  3238  rabrab  3265  ceqsex3v  3398  ceqsrex2v  3488  rexrab  3522  rexrab2  3526  2reu5  3568  rexss  3818  inass  3972  indifdir  4032  difin2  4038  difrab  4049  reupick3  4060  inssdif0  4094  rexdifpr  4344  rexdifsn  4460  reusv2lem4  5001  reusv2  5003  eqvinop  5082  copsexg  5083  wefrc  5243  rabxp  5294  elvvv  5318  resopab2  5589  difxp  5699  ssrnres  5713  mptpreima  5772  coass  5798  wfi  5856  imadif  6113  dff1o2  6283  eqfnfv3  6456  f1ossf1o  6538  isoini  6731  f1oiso  6744  oprabid  6822  dfoprab2  6848  mpt2eq123  6861  mpt2mptx  6898  resoprab2  6904  ov3  6944  uniuni  7118  elxp4  7257  elxp5  7258  oprabex3  7304  frxp  7438  rexsupp  7464  brtpos2  7510  oeeui  7836  oeeu  7837  omabs  7881  mapsnend  8188  xpsnen  8200  xpcomco  8206  xpassen  8210  wemapsolem  8611  epfrs  8771  bnd2  8920  aceq1  9140  dfac5lem1  9146  dfac5lem2  9147  dfac5lem5  9150  kmlem3  9176  kmlem14  9187  pwfseqlem1  9682  ltexpi  9926  ltexprlem4  10063  axaddf  10168  axmulf  10169  rexuz  11940  rexuz2  11941  nnwos  11958  zmin  11987  rexrp  12056  elixx3g  12393  elfz2  12540  preduz  12669  fzind2  12794  hashbclem  13438  resqrex  14199  rlim  14434  divalglem10  15333  divalgb  15335  gcdass  15472  lcmass  15535  isprm2  15602  infpn2  15824  ispos2  17156  issubg3  17820  resscntz  17971  subgdmdprd  18641  dprd2d2  18651  dfrhm2  18927  isassa  19530  aspval2  19562  fvmptnn04if  20874  ntreq0  21102  cmpcov2  21414  llyi  21498  nllyi  21499  subislly  21505  ptpjpre1  21595  tx1cn  21633  tx2cn  21634  txtube  21664  txkgen  21676  trfil2  21911  elflim2  21988  cnpflfi  22023  isfcls  22033  cnextcn  22091  istlm  22208  blres  22456  metrest  22549  isnlm  22699  elcncf1di  22918  elpi1  23064  isclmp  23116  iscvsp  23147  isncvsngp  23168  iscph  23189  cfilucfil3  23336  itg1climres  23701  itgsubst  24032  ulmdvlem3  24376  cubic  24797  vmasum  25162  logfac2  25163  lgsquadlem1  25326  lgsquadlem2  25327  legov  25701  ltgov  25713  perpln1  25826  axcontlem5  26069  nbgrel  26456  nbgrelOLD  26457  nbusgredgeu0  26493  nb3grpr2  26508  finsumvtxdg2ssteplem3  26678  usgr2pth0  26896  isclwlke  26908  wwlksnfi  27050  wlksnwwlknvbijOLD  27053  elwwlks2ons3  27102  elwwlks2ons3OLD  27103  wpthswwlks2on  27109  wpthswwlks2onOLD  27110  usgr2wspthon  27114  rusgrnumwwlkl1  27117  isclwwlk  27134  isclwwlknx  27191  clwlknf1oclwwlkn  27255  clwwlknonel  27269  clwwlknon2x  27278  clwwlkvbij  27289  clwwlkvbijOLDOLD  27290  clwwlkvbijOLD  27291  iseupthf1o  27382  fusgr2wsp2nb  27516  grpoidinvlem3  27700  h2hlm  28177  issh  28405  issh3  28416  ocsh  28482  cvbr2  29482  cvnbtwn2  29486  mdsl2i  29521  cvmdi  29523  mdsymlem2  29603  sumdmdii  29614  spc2ed  29652  difrab2  29677  disjunsn  29745  mpt2mptxf  29817  1stpreima  29824  2ndpreima  29825  f1od2  29839  nndiffz1  29888  omndmul2  30052  smatrcl  30202  crefdf  30255  pcmplfin  30267  1stmbfm  30662  2ndmbfm  30663  dya2iocnei  30684  eulerpartlemgvv  30778  eulerpartlemn  30783  bnj250  31107  bnj251  31108  bnj256  31112  bnj168  31136  iscvm  31579  axacprim  31922  dfpo2  31983  dfdm5  32012  dfrn5  32013  elima4  32015  imaindm  32018  frpoind  32077  frind  32080  sltval2  32146  madeval2  32273  dfon3  32336  brimg  32381  dfrecs2  32394  dfrdg4  32395  ifscgr  32488  cgrxfr  32499  segcon2  32549  seglecgr12im  32554  segletr  32558  ellines  32596  neifg  32703  bj-dfmpt2a  33403  topdifinffinlem  33532  icorempt2  33536  finxpreclem6  33570  wl-cases2-dnf  33632  curf  33720  uncf  33721  matunitlindflem2  33739  matunitlindf  33740  poimirlem26  33768  poimirlem28  33770  poimirlem30  33772  poimirlem32  33774  poimir  33775  itg2addnc  33796  ftc1anclem5  33821  ftc1anc  33825  areacirclem5  33836  isbnd2  33914  heibor1  33941  anan  34344  inxpxrn  34495  prtlem70  34664  prtlem100  34667  lsateln0  34804  islshpat  34826  lcvbr2  34831  lcvnbtwn2  34836  isopos  34989  cvrval2  35083  cvrnbtwn2  35084  ishlat2  35162  3dim0  35265  islvol5  35387  pmapjat1  35661  pclcmpatN  35709  pclfinclN  35758  cdlemefrs29pre00  36204  cdlemefrs29bpre0  36205  cdlemefrs29cpre1  36207  cdleme32a  36250  cdlemftr3  36374  dvhopellsm  36927  dibelval3  36957  diblsmopel  36981  mapdvalc  37439  mapdval4N  37442  mapdordlem1a  37444  diophrex  37865  rmxdioph  38109  dford4  38122  islmodfg  38165  islssfg2  38167  isdomn3  38308  fgraphopab  38314  k0004lem1  38971  2sbc5g  39143  limcrecl  40379  dvnmul  40676  dvnprodlem2  40680  fourierdlem83  40923  iundjiun  41194  4an21  41810  sprvalpwn0  42261  isrnghm  42420  isrnghmmul  42421  rngcinv  42509  rngcinvALTV  42521  ringcinv  42560  ringcinvALTV  42584  mpt2mptx2  42641
  Copyright terms: Public domain W3C validator