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

Theorem anass 472
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 471 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 470 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 212 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  bianass  641  an31  647  an4  655  3anass  1092  3an4anass  1102  an33rean  1480  2sb5  2284  r19.41v  3339  r19.41  3340  rabrab  3371  ceqsex3v  3531  spc2ed  3588  ceqsrex2v  3637  rexrab  3673  rexrab2  3679  2reu5  3735  rexss  4024  inass  4181  rexin  4201  indifdir  4245  difin2  4251  difrab  4262  reupick3  4273  inssdif0  4312  rexdifpr  4583  rexdifsn  4712  reusv2lem4  5290  reusv2  5292  eqvinop  5366  copsexgw  5369  copsexg  5370  rabxp  5588  elvvv  5615  resopab2  5892  difxp  6009  mptpreima  6080  resco  6091  coass  6106  wfi  6169  imadif  6427  dff1o2  6609  eqfnfv3  6793  f1ossf1o  6879  isoini  7081  f1oiso  7094  oprabidw  7177  oprabid  7178  dfoprab2  7202  mpoeq123  7216  mpomptx  7255  resoprab2  7261  ov3  7302  uniuni  7475  elxp4  7619  elxp5  7620  oprabex3  7670  frxp  7812  rexsupp  7840  brtpos2  7890  oeeui  8220  oeeu  8221  omabs  8266  mapsnend  8580  xpsnen  8593  xpcomco  8599  xpassen  8603  wemapsolem  9007  epfrs  9166  aceq1  9537  dfac5lem1  9543  dfac5lem2  9544  dfac5lem5  9547  kmlem3  9572  kmlem14  9583  pwfseqlem1  10074  ltexpi  10318  ltexprlem4  10455  axaddf  10561  axmulf  10562  rexuz  12293  rexuz2  12294  nnwos  12310  zmin  12339  rexrp  12405  elixx3g  12746  elfz2  12899  preduz  13031  fzind2  13157  hashbclem  13813  resqrex  14608  rlim  14850  divalglem10  15749  divalgb  15751  gcdass  15891  lcmass  15954  isprm2  16022  infpn2  16245  ispos2  17556  issubmndb  17968  issubg3  18295  resscntz  18460  subgdmdprd  19154  dprd2d2  19164  dfrhm2  19467  isassa  20083  aspval2  20122  fvmptnn04if  21452  ntreq0  21680  cmpcov2  21993  llyi  22077  nllyi  22078  ptpjpre1  22174  tx1cn  22212  tx2cn  22213  txtube  22243  txkgen  22255  trfil2  22490  elflim2  22567  cnpflfi  22602  isfcls  22612  cnextcn  22670  istlm  22788  blres  23036  metrest  23129  isnlm  23279  elpi1  23648  isclmp  23700  iscvsp  23731  isncvsngp  23752  iscph  23773  cfilucfil3  23922  itg1climres  24316  itgsubst  24650  ulmdvlem3  24995  cubic  25433  vmasum  25798  lgsquadlem1  25962  lgsquadlem2  25963  legov  26377  perpln1  26502  axcontlem5  26760  nbgrel  27128  nbusgredgeu0  27156  nb3grpr2  27171  finsumvtxdg2ssteplem3  27335  usgr2pth0  27552  isclwlke  27564  wwlksnfi  27690  elwwlks2ons3  27739  wpthswwlks2on  27745  usgr2wspthon  27749  rusgrnumwwlkl1  27752  isclwwlk  27767  isclwwlknx  27819  clwlknf1oclwwlkn  27867  clwwlknonel  27878  clwwlknon2x  27886  clwwlkvbij  27896  iseupthf1o  27985  fusgr2wsp2nb  28117  grpoidinvlem3  28287  h2hlm  28761  issh  28989  issh3  29000  ocsh  29064  cvbr2  30064  cvnbtwn2  30068  mdsl2i  30103  cvmdi  30105  mdsymlem2  30185  sumdmdii  30196  dmrab  30264  difrab2  30265  disjunsn  30350  mpomptxf  30431  1stpreima  30448  2ndpreima  30449  f1od2  30463  nndiffz1  30515  omndmul2  30740  smatrcl  31091  crefdf  31142  1stmbfm  31545  2ndmbfm  31546  dya2iocnei  31567  eulerpartlemgvv  31661  eulerpartlemn  31666  bnj250  31998  bnj251  31999  bnj256  32003  bnj168  32027  cusgr3cyclex  32410  iscvm  32533  axacprim  32960  dfpo2  33018  dfdm5  33043  dfrn5  33044  elima4  33046  frpoind  33107  frind  33112  sltval2  33190  madeval2  33317  dfon3  33380  brimg  33425  dfrecs2  33438  dfrdg4  33439  ifscgr  33532  cgrxfr  33543  segcon2  33593  seglecgr12im  33598  segletr  33602  ellines  33640  neifg  33746  bj-dfmpoa  34448  bj-imdiridlem  34515  bj-imdirco  34520  topdifinffinlem  34678  icorempo  34682  difunieq  34705  finxpreclem6  34727  wl-cases2-dnf  34829  curf  34947  uncf  34948  matunitlindflem2  34966  matunitlindf  34967  poimirlem26  34995  poimirlem28  34997  poimirlem30  34999  poimirlem32  35001  poimir  35002  itg2addnc  35023  ftc1anclem5  35046  ftc1anc  35050  areacirclem5  35061  isbnd2  35133  heibor1  35160  anan  35571  inxpxrn  35715  prtlem70  36065  prtlem100  36067  lsateln0  36203  islshpat  36225  lcvbr2  36230  lcvnbtwn2  36235  isopos  36388  cvrval2  36482  cvrnbtwn2  36483  ishlat2  36561  3dim0  36665  islvol5  36787  pmapjat1  37061  pclcmpatN  37109  pclfinclN  37158  cdlemefrs29pre00  37603  cdlemefrs29bpre0  37604  cdlemefrs29cpre1  37606  cdleme32a  37649  cdlemftr3  37773  dvhopellsm  38325  dibelval3  38355  diblsmopel  38379  mapdvalc  38837  mapdval4N  38840  mapdordlem1a  38842  3factsumint2  39218  3factsumint3  39219  3factsumint4  39220  3factsumint  39221  diophrex  39572  rmxdioph  39813  dford4  39826  islmodfg  39869  islssfg2  39871  isdomn3  40004  fgraphopab  40010  k0004lem1  40709  ismnuprim  40862  2sbc5g  40980  limcrecl  42137  dvnmul  42451  dvnprodlem2  42455  fourierdlem83  42697  iundjiun  42965  4an21  43692  sprvalpwn0  43866  pairreueq  43893  prprsprreu  43902  prprreueq  43903  isrnghm  44382  isrnghmmul  44383  rngcinv  44471  rngcinvALTV  44483  ringcinv  44522  ringcinvALTV  44546  mpomptx2  44602
  Copyright terms: Public domain W3C validator