Theorem anass 681

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	|- ( ( ( 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 680	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 22	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 679	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) /\ ch ) )
5	2, 4	impbii 199	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

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  838  an32  839  an13  840  an31  841  bianass  842  an4  865  3anass  1042  3an4anass  1291  2sb5  2443  r19.41v  3089  r19.41  3090  ceqsex3v  3246  ceqsrex2v  3338  rexrab  3370  rexrab2  3374  2reu5  3416  rexss  3669  inass  3823  indifdir  3883  difin2  3890  difrab  3901  reupick3  3912  inssdif0  3947  rexdifpr  4205  rexdifsn  4323  reusv2lem4  4872  reusv2  4874  eqvinop  4955  copsexg  4956  wefrc  5108  rabxp  5154  elvvv  5178  resopab2  5448  difxp  5558  ssrnres  5572  mptpreima  5628  coass  5654  wfi  5713  imadif  5973  dff1o2  6142  eqfnfv3  6313  isoini  6588  f1oiso  6601  oprabid  6677  dfoprab2  6701  mpt2eq123  6714  mpt2mptx  6751  resoprab2  6757  ov3  6797  uniuni  6971  elxp4  7110  elxp5  7111  oprabex3  7157  frxp  7287  rexsupp  7313  brtpos2  7358  oeeui  7682  oeeu  7683  omabs  7727  mapsnen  8035  xpsnen  8044  xpcomco  8050  xpassen  8054  wemapsolem  8455  epfrs  8607  bnd2  8756  aceq1  8940  dfac5lem1  8946  dfac5lem2  8947  dfac5lem5  8950  kmlem3  8974  kmlem14  8985  pwfseqlem1  9480  ltexpi  9724  ltexprlem4  9861  axaddf  9966  axmulf  9967  rexuz  11738  rexuz2  11739  nnwos  11755  zmin  11784  rexrp  11853  elixx3g  12188  elfz2  12333  preduz  12461  fzind2  12586  hashbclem  13236  resqrex  13991  rlim  14226  divalglem10  15125  divalgb  15127  gcdass  15264  lcmass  15327  isprm2  15395  infpn2  15617  ispos2  16948  issubg3  17612  resscntz  17764  subgdmdprd  18433  dprd2d2  18443  dfrhm2  18717  isassa  19315  aspval2  19347  fvmptnn04if  20654  ntreq0  20881  cmpcov2  21193  llyi  21277  nllyi  21278  subislly  21284  ptpjpre1  21374  tx1cn  21412  tx2cn  21413  txtube  21443  txkgen  21455  trfil2  21691  elflim2  21768  cnpflfi  21803  isfcls  21813  cnextcn  21871  istlm  21988  blres  22236  metrest  22329  isnlm  22479  elcncf1di  22698  elpi1  22845  isclmp  22897  iscvsp  22928  isncvsngp  22949  iscph  22970  cfilucfil3  23117  itg1climres  23481  itgsubst  23812  ulmdvlem3  24156  cubic  24576  vmasum  24941  logfac2  24942  lgsquadlem1  25105  lgsquadlem2  25106  legov  25480  ltgov  25492  perpln1  25605  axcontlem5  25848  nbgrel  26238  nbusgredgeu0  26270  nb3grpr2  26285  finsumvtxdg2ssteplem3  26443  usgr2pth0  26661  isclwlke  26673  wwlksnfi  26801  wlksnwwlknvbij  26803  elwwlks2ons3  26848  wpthswwlks2on  26854  usgr2wspthon  26858  rusgrnumwwlkl1  26863  isclwwlks  26880  isclwwlksnx  26889  clwwlksvbij  26922  iseupthf1o  27062  fusgr2wsp2nb  27198  numclwwlkovf2  27217  grpoidinvlem3  27360  h2hlm  27837  issh  28065  issh3  28076  ocsh  28142  cvbr2  29142  cvnbtwn2  29146  mdsl2i  29181  cvmdi  29183  mdsymlem2  29263  sumdmdii  29274  spc2ed  29312  rabrab  29338  difrab2  29339  disjunsn  29407  mpt2mptxf  29477  1stpreima  29484  2ndpreima  29485  f1od2  29499  nndiffz1  29548  omndmul2  29712  smatrcl  29862  crefdf  29915  pcmplfin  29927  1stmbfm  30322  2ndmbfm  30323  dya2iocnei  30344  eulerpartlemgvv  30438  eulerpartlemn  30443  bnj250  30767  bnj251  30768  bnj256  30772  bnj168  30798  iscvm  31241  axacprim  31584  dfpo2  31645  dfdm5  31676  dfrn5  31677  elima4  31679  imaindm  31682  frind  31740  sltval2  31809  madeval2  31936  dfon3  31999  brimg  32044  dfrecs2  32057  dfrdg4  32058  ifscgr  32151  cgrxfr  32162  segcon2  32212  seglecgr12im  32217  segletr  32221  ellines  32259  neifg  32366  bj-dfmpt2a  33071  topdifinffinlem  33195  icorempt2  33199  finxpreclem6  33233  wl-cases2-dnf  33295  curf  33387  uncf  33388  matunitlindflem2  33406  matunitlindf  33407  poimirlem26  33435  poimirlem28  33437  poimirlem30  33439  poimirlem32  33441  poimir  33442  itg2addnc  33464  ftc1anclem5  33489  ftc1anc  33493  areacirclem5  33504  isbnd2  33582  heibor1  33609  anan  33999  prtlem70  34141  prtlem100  34144  lsateln0  34282  islshpat  34304  lcvbr2  34309  lcvnbtwn2  34314  isopos  34467  cvrval2  34561  cvrnbtwn2  34562  ishlat2  34640  3dim0  34743  islvol5  34865  pmapjat1  35139  pclcmpatN  35187  pclfinclN  35236  cdlemefrs29pre00  35683  cdlemefrs29bpre0  35684  cdlemefrs29cpre1  35686  cdleme32a  35729  cdlemftr3  35853  dvhopellsm  36406  dibelval3  36436  diblsmopel  36460  mapdvalc  36918  mapdval4N  36921  mapdordlem1a  36923  diophrex  37339  rmxdioph  37583  dford4  37596  islmodfg  37639  islssfg2  37641  isdomn3  37782  fgraphopab  37788  k0004lem1  38445  2sbc5g  38617  mapsnend  39391  limcrecl  39861  dvnmul  40158  dvnprodlem2  40162  fourierdlem83  40406  iundjiun  40677  sprvalpwn0  41733  isrnghm  41892  isrnghmmul  41893  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  mpt2mptx2  42113