ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anass Structured version   Unicode version

Theorem anass 381
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
anass

Proof of Theorem anass
StepHypRef Expression
1 id 19 . . 3
21anassrs 380 . 2
3 id 19 . . 3
43anasss 379 . 2
52, 4impbii 117 1
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpan10  443  an12  495  an32  496  an13  497  an31  498  an4  520  3anass  888  sbidm  1728  4exdistr  1790  2sb5  1856  2sb5rf  1862  sbel2x  1871  r2exf  2336  r19.41  2459  ceqsex3v  2590  ceqsrex2v  2670  rexrab  2698  rexrab2  2702  rexss  3001  inass  3141  difin2  3193  difrab  3205  reupick3  3216  inssdif0im  3285  rexdifsn  3490  unidif0  3911  bnd2  3917  eqvinop  3971  copsexg  3972  uniuni  4149  rabxp  4323  elvvv  4346  rexiunxp  4421  resopab2  4598  ssrnres  4706  elxp4  4751  elxp5  4752  cnvresima  4753  mptpreima  4757  coass  4782  dff1o2  5074  eqfnfv3  5210  rexsupp  5234  isoini  5400  f1oiso  5408  oprabid  5480  dfoprab2  5494  mpt2eq123  5506  mpt2mptx  5537  resoprab2  5540  ovi3  5579  oprabex3  5698  brtpos2  5807  xpsnen  6231  xpcomco  6236  xpassen  6240  ltexpi  6321  enq0enq  6413  enq0tr  6416  prnmaxl  6470  prnminu  6471  genpdflem  6489  ltexprlemm  6572  rexuz  8259  rexuz2  8260  rexrp  8340  elixx3g  8500  elfz2  8611  fzdifsuc  8673  fzind2  8825
  Copyright terms: Public domain W3C validator