Theorem anass 642

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	|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Proof of Theorem anass

Step	Hyp	Ref	Expression
1		id 22	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ph /\ ( ps /\ ch ) ) )
2	1	anassrs 641	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 22	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 640	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) /\ ch ) )
5	2, 4	impbii 188	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  an12  788  an32  789  an13  790  an31  791  an4  813  3anass  962  2sb5  2151  2sb5rfOLD  2163  sbel2xOLD  2172  r2exf  2741  r19.41  2862  ceqsex3v  3001  ceqsrex2v  3084  rexrab  3112  rexrab2  3116  2reu5  3156  rexss  3407  inass  3548  indifdir  3594  difin2  3600  difrab  3612  reupick3  3623  inssdif0  3734  rexdifsn  3992  reusv2lem4  4484  reusv2  4486  eqvinop  4563  copsexg  4564  copsexgOLD  4565  wefrc  4701  rabxp  4862  elvvv  4885  resopab2  5143  difxp  5250  ssrnres  5264  cnvresima  5315  mptpreima  5319  coass  5344  imadif  5481  dff1o2  5634  eqfnfv3  5787  rexsuppOLD  5816  isoini  6016  f1oiso  6029  oprabid  6104  dfoprab2  6122  mpt2eq123  6134  mpt2mptx  6170  resoprab2  6176  ov3  6216  uniuni  6374  elxp4  6511  elxp5  6512  oprabex3  6555  frxp  6671  rexsupp  6696  brtpos2  6740  oeeui  7029  oeeu  7030  omabs  7074  mapsnen  7375  xpsnen  7383  xpcomco  7389  xpassen  7393  wemapsolem  7752  epfrs  7939  bnd2  8088  aceq1  8275  dfac5lem1  8281  dfac5lem2  8282  dfac5lem5  8285  kmlem3  8309  kmlem14  8320  pwfseqlem1  8813  ltexpi  9059  ltexprlem4  9196  axaddf  9300  axmulf  9301  rexuz  10893  rexuz2  10894  nnwos  10910  zmin  10937  rexrp  10998  elixx3g  11301  elfz2  11431  fzind2  11621  hashbclem  12189  resqrex  12724  rlim  12957  divalglem10  13589  divalgb  13591  gcdass  13712  isprm2  13754  infpn2  13957  ispos2  15101  issubg3  15679  resscntz  15829  subgdmdprd  16505  dprd2d2  16517  dfrhm2  16742  isassa  17309  aspval2  17339  istps2OLD  18368  istps3OLD  18369  ntreq0  18523  cmpcov2  18835  llyi  18920  nllyi  18921  subislly  18927  ptpjpre1  18986  tx1cn  19024  tx2cn  19025  txtube  19055  txkgen  19067  trfil2  19302  elflim2  19379  cnpflfi  19414  isfcls  19424  cnextcn  19481  istlm  19601  blres  19848  metrest  19941  isnlm  20098  elcncf1di  20313  elpi1  20459  iscph  20531  cfilucfil3OLD  20671  cfilucfil3  20672  itg1climres  21034  itgsubst  21363  ulmdvlem3  21752  cubic  22129  vmasum  22440  logfac2  22441  lgsquadlem1  22578  lgsquadlem2  22579  legov  22892  axcontlem5  23037  nb3grapr2  23185  trls  23258  3v3e3cycl2  23373  grpoidinvlem3  23516  h2hlm  24205  issh  24433  issh3  24445  ocsh  24509  cvbr2  25510  cvnbtwn2  25514  mdsl2i  25549  cvmdi  25551  mdsymlem2  25631  sumdmdii  25642  spc2ed  25680  rabrab  25708  disjunsn  25760  mpt2mptxf  25819  1stpreima  25825  2ndpreima  25826  f1od2  25848  nndiffz1  25898  1stmbfm  26529  2ndmbfm  26530  dya2iocnei  26551  eulerpartlemgvv  26607  eulerpartlemn  26612  iscvm  26996  axacprim  27205  dfpo2  27412  dfdm5  27434  dfrn5  27435  elima4  27437  preduz  27508  wfi  27515  frind  27551  sltval2  27644  nofulllem5  27694  dfon3  27770  brimg  27815  brsuccf  27819  dfrdg4  27828  tfrqfree  27829  ifscgr  27922  cgrxfr  27933  segcon2  27983  seglecgr12im  27988  segletr  27992  ellines  28030  itg2addnc  28290  ftc1anclem5  28315  ftc1anc  28319  areacirclem5  28332  neifg  28436  isbnd2  28526  heibor1  28553  mergeconj  28749  prtlem70  28841  prtlem100  28845  diophrex  28959  rmxdioph  29210  dford4  29223  islmodfg  29267  islssfg2  29269  isdomn3  29417  fgraphopab  29423  2sbc5g  29515  3an4anass  29961  rexdifpr  29970  usgra2pth0  30148  wwlknprop  30166  wwlkextwrd  30206  wwlknfi  30216  wlknwwlknvbij  30218  usg2spthonot0  30254  usg2spthonot1  30255  isclwlk  30267  clwwlkvbij  30309  rusgranumwlkl1  30405  rusgranumwlklem3  30415  rusgra0edg  30419  1to2vfriswmgra  30444  usgreg2spot  30506  numclwwlkovf2  30523  mpt2mptx2  30569  bnj250  31412  bnj251  31413  bnj256  31417  bnj168  31444  lsateln0  32234  islshpat  32256  lcvbr2  32261  lcvnbtwn2  32266  isopos  32419  cvrval2  32513  cvrnbtwn2  32514  ishlat2  32592  3dim0  32695  islvol5  32817  pmapjat1  33091  pclcmpatN  33139  pclfinclN  33188  cdlemefrs29pre00  33633  cdlemefrs29bpre0  33634  cdlemefrs29cpre1  33636  cdleme32a  33679  cdlemftr3  33803  dvhopellsm  34356  dibelval3  34386  diblsmopel  34410  mapdvalc  34868  mapdval4N  34871  mapdordlem1a  34873