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

Theorem anass 684
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 683 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 682 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 199 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  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 197  df-an 385
This theorem is referenced by:  an12  873  an32  874  an13  875  an31  876  bianass  877  an4  900  3anass  1081  3an4anass  1094  2sb5  2580  r19.41v  3227  r19.41  3228  rabrab  3255  ceqsex3v  3386  ceqsrex2v  3477  rexrab  3511  rexrab2  3515  2reu5  3557  rexss  3810  inass  3966  indifdir  4026  difin2  4033  difrab  4044  reupick3  4055  inssdif0  4090  rexdifpr  4350  rexdifsn  4469  reusv2lem4  5021  reusv2  5023  eqvinop  5103  copsexg  5104  wefrc  5260  rabxp  5311  elvvv  5335  resopab2  5606  difxp  5716  ssrnres  5730  mptpreima  5789  coass  5815  wfi  5874  imadif  6134  dff1o2  6304  eqfnfv3  6477  isoini  6752  f1oiso  6765  oprabid  6841  dfoprab2  6867  mpt2eq123  6880  mpt2mptx  6917  resoprab2  6923  ov3  6963  uniuni  7137  elxp4  7276  elxp5  7277  oprabex3  7323  frxp  7456  rexsupp  7482  brtpos2  7528  oeeui  7853  oeeu  7854  omabs  7898  mapsnen  8202  xpsnen  8211  xpcomco  8217  xpassen  8221  wemapsolem  8622  epfrs  8782  bnd2  8931  aceq1  9150  dfac5lem1  9156  dfac5lem2  9157  dfac5lem5  9160  kmlem3  9186  kmlem14  9197  pwfseqlem1  9692  ltexpi  9936  ltexprlem4  10073  axaddf  10178  axmulf  10179  rexuz  11951  rexuz2  11952  nnwos  11968  zmin  11997  rexrp  12066  elixx3g  12401  elfz2  12546  preduz  12675  fzind2  12800  hashbclem  13448  resqrex  14210  rlim  14445  divalglem10  15347  divalgb  15349  gcdass  15486  lcmass  15549  isprm2  15617  infpn2  15839  ispos2  17169  issubg3  17833  resscntz  17984  subgdmdprd  18653  dprd2d2  18663  dfrhm2  18939  isassa  19537  aspval2  19569  fvmptnn04if  20876  ntreq0  21103  cmpcov2  21415  llyi  21499  nllyi  21500  subislly  21506  ptpjpre1  21596  tx1cn  21634  tx2cn  21635  txtube  21665  txkgen  21677  trfil2  21912  elflim2  21989  cnpflfi  22024  isfcls  22034  cnextcn  22092  istlm  22209  blres  22457  metrest  22550  isnlm  22700  elcncf1di  22919  elpi1  23065  isclmp  23117  iscvsp  23148  isncvsngp  23169  iscph  23190  cfilucfil3  23337  itg1climres  23700  itgsubst  24031  ulmdvlem3  24375  cubic  24796  vmasum  25161  logfac2  25162  lgsquadlem1  25325  lgsquadlem2  25326  legov  25700  ltgov  25712  perpln1  25825  axcontlem5  26068  nbgrel  26453  nbgrelOLD  26454  nbusgredgeu0  26489  nb3grpr2  26504  finsumvtxdg2ssteplem3  26674  usgr2pth0  26892  isclwlke  26904  wwlksnfi  27045  wlksnwwlknvbij  27047  elwwlks2ons3  27096  elwwlks2ons3OLD  27097  wpthswwlks2on  27103  wpthswwlks2onOLD  27104  usgr2wspthon  27108  rusgrnumwwlkl1  27111  isclwwlk  27128  isclwwlknx  27185  clwlknf1oclwwlkn  27249  clwwlknonel  27263  clwwlknon2x  27272  clwwlkvbij  27283  clwwlkvbijOLD  27284  iseupthf1o  27375  fusgr2wsp2nb  27509  grpoidinvlem3  27690  h2hlm  28167  issh  28395  issh3  28406  ocsh  28472  cvbr2  29472  cvnbtwn2  29476  mdsl2i  29511  cvmdi  29513  mdsymlem2  29593  sumdmdii  29604  spc2ed  29642  difrab2  29667  disjunsn  29735  mpt2mptxf  29807  1stpreima  29814  2ndpreima  29815  f1od2  29829  nndiffz1  29878  omndmul2  30042  smatrcl  30192  crefdf  30245  pcmplfin  30257  1stmbfm  30652  2ndmbfm  30653  dya2iocnei  30674  eulerpartlemgvv  30768  eulerpartlemn  30773  bnj250  31097  bnj251  31098  bnj256  31102  bnj168  31126  iscvm  31569  axacprim  31912  dfpo2  31973  dfdm5  32002  dfrn5  32003  elima4  32005  imaindm  32008  frpoind  32067  frind  32070  sltval2  32136  madeval2  32263  dfon3  32326  brimg  32371  dfrecs2  32384  dfrdg4  32385  ifscgr  32478  cgrxfr  32489  segcon2  32539  seglecgr12im  32544  segletr  32548  ellines  32586  neifg  32693  bj-dfmpt2a  33395  topdifinffinlem  33524  icorempt2  33528  finxpreclem6  33562  wl-cases2-dnf  33626  curf  33718  uncf  33719  matunitlindflem2  33737  matunitlindf  33738  poimirlem26  33766  poimirlem28  33768  poimirlem30  33770  poimirlem32  33772  poimir  33773  itg2addnc  33795  ftc1anclem5  33820  ftc1anc  33824  areacirclem5  33835  isbnd2  33913  heibor1  33940  anan  34343  inxpxrn  34494  prtlem70  34663  prtlem100  34666  lsateln0  34803  islshpat  34825  lcvbr2  34830  lcvnbtwn2  34835  isopos  34988  cvrval2  35082  cvrnbtwn2  35083  ishlat2  35161  3dim0  35264  islvol5  35386  pmapjat1  35660  pclcmpatN  35708  pclfinclN  35757  cdlemefrs29pre00  36203  cdlemefrs29bpre0  36204  cdlemefrs29cpre1  36206  cdleme32a  36249  cdlemftr3  36373  dvhopellsm  36926  dibelval3  36956  diblsmopel  36980  mapdvalc  37438  mapdval4N  37441  mapdordlem1a  37443  diophrex  37859  rmxdioph  38103  dford4  38116  islmodfg  38159  islssfg2  38161  isdomn3  38302  fgraphopab  38308  k0004lem1  38965  2sbc5g  39137  mapsnend  39908  limcrecl  40382  dvnmul  40679  dvnprodlem2  40683  fourierdlem83  40927  iundjiun  41198  4an21  41814  sprvalpwn0  42261  isrnghm  42420  isrnghmmul  42421  rngcinv  42509  rngcinvALTV  42521  ringcinv  42560  ringcinvALTV  42584  mpt2mptx2  42641
  Copyright terms: Public domain W3C validator