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

Theorem anass 680
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 679 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 678 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 199 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 386
This theorem is referenced by:  an12  837  an32  838  an13  839  an31  840  bianass  841  an4  864  3anass  1040  3an4anass  1288  2sb5  2442  r19.41v  3081  r19.41  3082  ceqsex3v  3232  ceqsrex2v  3321  rexrab  3352  rexrab2  3356  2reu5  3398  rexss  3648  inass  3801  indifdir  3859  difin2  3866  difrab  3877  reupick3  3888  inssdif0  3921  rexdifpr  4176  rexdifsn  4292  reusv2lem4  4832  reusv2  4834  eqvinop  4915  copsexg  4916  wefrc  5068  rabxp  5114  elvvv  5139  resopab2  5407  difxp  5517  ssrnres  5531  mptpreima  5587  coass  5613  wfi  5672  imadif  5931  dff1o2  6099  eqfnfv3  6269  isoini  6542  f1oiso  6555  oprabid  6631  dfoprab2  6654  mpt2eq123  6667  mpt2mptx  6704  resoprab2  6710  ov3  6750  uniuni  6920  elxp4  7057  elxp5  7058  oprabex3  7102  frxp  7232  rexsupp  7258  brtpos2  7303  oeeui  7627  oeeu  7628  omabs  7672  mapsnen  7979  xpsnen  7988  xpcomco  7994  xpassen  7998  wemapsolem  8399  epfrs  8551  bnd2  8700  aceq1  8884  dfac5lem1  8890  dfac5lem2  8891  dfac5lem5  8894  kmlem3  8918  kmlem14  8929  pwfseqlem1  9424  ltexpi  9668  ltexprlem4  9805  axaddf  9910  axmulf  9911  rexuz  11682  rexuz2  11683  nnwos  11699  zmin  11728  rexrp  11797  elixx3g  12130  elfz2  12275  preduz  12402  fzind2  12526  hashbclem  13174  resqrex  13925  rlim  14160  divalglem10  15049  divalgb  15051  gcdass  15188  lcmass  15251  isprm2  15319  infpn2  15541  ispos2  16869  issubg3  17533  resscntz  17685  subgdmdprd  18354  dprd2d2  18364  dfrhm2  18638  isassa  19234  aspval2  19266  fvmptnn04if  20573  ntreq0  20791  cmpcov2  21103  llyi  21187  nllyi  21188  subislly  21194  ptpjpre1  21284  tx1cn  21322  tx2cn  21323  txtube  21353  txkgen  21365  trfil2  21601  elflim2  21678  cnpflfi  21713  isfcls  21723  cnextcn  21781  istlm  21898  blres  22146  metrest  22239  isnlm  22389  elcncf1di  22606  elpi1  22753  isclmp  22805  iscvsp  22836  isncvsngp  22857  iscph  22878  cfilucfil3  23025  itg1climres  23387  itgsubst  23716  ulmdvlem3  24060  cubic  24476  vmasum  24841  logfac2  24842  lgsquadlem1  25005  lgsquadlem2  25006  legov  25380  ltgov  25392  perpln1  25505  axcontlem5  25748  nbgrel  26125  nbusgredgeu0  26157  nb3grpr2  26172  usgr2pth0  26530  isclwlke  26542  wwlksnfi  26670  wlksnwwlknvbij  26672  elwwlks2ons3  26717  wpthswwlks2on  26722  usgr2wspthon  26726  rusgrnumwwlkl1  26730  isclwwlks  26747  isclwwlksnx  26756  clwwlksvbij  26788  iseupthf1o  26928  numclwwlkovf2  27073  grpoidinvlem3  27209  h2hlm  27686  issh  27914  issh3  27925  ocsh  27991  cvbr2  28991  cvnbtwn2  28995  mdsl2i  29030  cvmdi  29032  mdsymlem2  29112  sumdmdii  29123  spc2ed  29161  rabrab  29187  disjunsn  29252  mpt2mptxf  29320  1stpreima  29327  2ndpreima  29328  f1od2  29342  nndiffz1  29390  omndmul2  29497  smatrcl  29644  crefdf  29697  pcmplfin  29709  1stmbfm  30103  2ndmbfm  30104  dya2iocnei  30125  eulerpartlemgvv  30219  eulerpartlemn  30224  bnj250  30474  bnj251  30475  bnj256  30479  bnj168  30506  iscvm  30949  axacprim  31292  dfpo2  31353  dfdm5  31378  dfrn5  31379  elima4  31381  frind  31441  sltval2  31510  dfon3  31641  brimg  31686  dfrecs2  31699  dfrdg4  31700  ifscgr  31793  cgrxfr  31804  segcon2  31854  seglecgr12im  31859  segletr  31863  ellines  31901  neifg  32008  bj-dfmpt2a  32708  topdifinffinlem  32827  icorempt2  32831  finxpreclem6  32865  wl-cases2-dnf  32927  curf  33019  uncf  33020  matunitlindflem2  33038  matunitlindf  33039  poimirlem26  33067  poimirlem28  33069  poimirlem30  33071  poimirlem32  33073  poimir  33074  itg2addnc  33096  ftc1anclem5  33121  ftc1anc  33125  areacirclem5  33136  isbnd2  33214  heibor1  33241  prtlem70  33619  prtlem100  33623  lsateln0  33762  islshpat  33784  lcvbr2  33789  lcvnbtwn2  33794  isopos  33947  cvrval2  34041  cvrnbtwn2  34042  ishlat2  34120  3dim0  34223  islvol5  34345  pmapjat1  34619  pclcmpatN  34667  pclfinclN  34716  cdlemefrs29pre00  35163  cdlemefrs29bpre0  35164  cdlemefrs29cpre1  35166  cdleme32a  35209  cdlemftr3  35333  dvhopellsm  35886  dibelval3  35916  diblsmopel  35940  mapdvalc  36398  mapdval4N  36401  mapdordlem1a  36403  diophrex  36819  rmxdioph  37063  dford4  37076  islmodfg  37119  islssfg2  37121  isdomn3  37263  fgraphopab  37269  k0004lem1  37927  2sbc5g  38099  mapsnend  38865  limcrecl  39265  dvnmul  39464  dvnprodlem2  39468  fourierdlem83  39713  iundjiun  39984  sprvalpwn0  41021  isrnghm  41180  isrnghmmul  41181  rngcinv  41269  rngcinvALTV  41281  ringcinv  41320  ringcinvALTV  41344  mpt2mptx2  41401
  Copyright terms: Public domain W3C validator