Theorem anass 649

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 648	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 22	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 647	. 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  795  an32  796  an13  797  an31  798  an4  822  3anass  976  3an4anass  1218  2sb5  2171  r2exfOLD  2963  r19.41  2993  ceqsex3v  3133  ceqsrex2v  3219  rexrab  3247  rexrab2  3251  2reu5  3292  rexss  3549  inass  3690  indifdir  3736  difin2  3742  difrab  3754  reupick3  3765  inssdif0  3877  rexdifsn  4140  reusv2lem4  4637  reusv2  4639  eqvinop  4717  copsexg  4718  copsexgOLD  4719  wefrc  4859  rabxp  5022  elvvv  5045  resopab2  5308  difxp  5417  ssrnres  5431  cnvresima  5482  mptpreima  5486  coass  5512  imadif  5649  dff1o2  5807  eqfnfv3  5964  rexsuppOLD  5993  isoini  6215  f1oiso  6228  oprabid  6304  dfoprab2  6324  mpt2eq123  6337  mpt2mptx  6374  resoprab2  6380  ov3  6420  uniuni  6590  elxp4  6725  elxp5  6726  oprabex3  6770  frxp  6891  rexsupp  6916  brtpos2  6959  oeeui  7249  oeeu  7250  omabs  7294  mapsnen  7591  xpsnen  7599  xpcomco  7605  xpassen  7609  wemapsolem  7973  epfrs  8160  bnd2  8309  aceq1  8496  dfac5lem1  8502  dfac5lem2  8503  dfac5lem5  8506  kmlem3  8530  kmlem14  8541  pwfseqlem1  9034  ltexpi  9278  ltexprlem4  9415  axaddf  9520  axmulf  9521  rexuz  11135  rexuz2  11136  nnwos  11153  zmin  11182  rexrp  11243  elixx3g  11546  elfz2  11683  fzind2  11898  hashbclem  12475  resqrex  13058  rlim  13292  divalglem10  13932  divalgb  13934  gcdass  14055  isprm2  14097  infpn2  14303  ispos2  15446  issubg3  16088  resscntz  16238  subgdmdprd  16949  dprd2d2  16961  dfrhm2  17234  isassa  17832  aspval2  17864  fvmptnn04if  19217  istps2OLD  19289  istps3OLD  19290  ntreq0  19444  cmpcov2  19756  llyi  19841  nllyi  19842  subislly  19848  ptpjpre1  19938  tx1cn  19976  tx2cn  19977  txtube  20007  txkgen  20019  trfil2  20254  elflim2  20331  cnpflfi  20366  isfcls  20376  cnextcn  20433  istlm  20553  blres  20800  metrest  20893  isnlm  21050  elcncf1di  21265  elpi1  21411  iscph  21483  cfilucfil3OLD  21623  cfilucfil3  21624  itg1climres  21987  itgsubst  22316  ulmdvlem3  22662  cubic  23045  vmasum  23356  logfac2  23357  lgsquadlem1  23494  lgsquadlem2  23495  legov  23837  ltgov  23848  perpln1  23952  axcontlem5  24136  nb3grapr2  24319  trls  24403  3v3e3cycl2  24529  wwlknprop  24551  wwlkextwrd  24593  wwlknfi  24603  wlknwwlknvbij  24605  isclwlk  24621  clwwlkvbij  24666  usg2spthonot0  24754  usg2spthonot1  24755  rusgranumwlkl1  24812  rusgranumwlklem3  24816  rusgra0edg  24820  1to2vfriswmgra  24871  usgreg2spot  24932  numclwwlkovf2  24949  grpoidinvlem3  25073  h2hlm  25762  issh  25990  issh3  26002  ocsh  26066  cvbr2  27067  cvnbtwn2  27071  mdsl2i  27106  cvmdi  27108  mdsymlem2  27188  sumdmdii  27199  spc2ed  27237  rabrab  27264  disjunsn  27318  mpt2mptxf  27383  1stpreima  27389  2ndpreima  27390  f1od2  27412  nndiffz1  27461  omndmul2  27568  crefdf  27717  pcmplfin  27729  1stmbfm  28097  2ndmbfm  28098  dya2iocnei  28119  eulerpartlemgvv  28181  eulerpartlemn  28186  iscvm  28570  axacprim  28945  dfpo2  29152  dfdm5  29174  dfrn5  29175  elima4  29177  preduz  29248  wfi  29255  frind  29291  sltval2  29384  nofulllem5  29434  dfon3  29510  brimg  29555  brsuccf  29559  dfrdg4  29568  tfrqfree  29569  ifscgr  29662  cgrxfr  29673  segcon2  29723  seglecgr12im  29728  segletr  29732  ellines  29770  itg2addnc  30037  ftc1anclem5  30062  ftc1anc  30066  areacirclem5  30079  neifg  30157  isbnd2  30247  heibor1  30274  mergeconj  30470  prtlem70  30560  prtlem100  30564  diophrex  30677  rmxdioph  30926  dford4  30939  islmodfg  30983  islssfg2  30985  isdomn3  31133  fgraphopab  31139  lcmass  31187  2sbc5g  31270  limcrecl  31539  fourierdlem83  31857  rexdifpr  32134  usgra2pth0  32189  isrnghm  32406  isrnghmmul  32407  rngcinv  32508  rngcinvOLD  32520  ringcinv  32553  ringcinvOLD  32576  mpt2mptx2  32632  bnj250  33461  bnj251  33462  bnj256  33466  bnj168  33493  lsateln0  34422  islshpat  34444  lcvbr2  34449  lcvnbtwn2  34454  isopos  34607  cvrval2  34701  cvrnbtwn2  34702  ishlat2  34780  3dim0  34883  islvol5  35005  pmapjat1  35279  pclcmpatN  35327  pclfinclN  35376  cdlemefrs29pre00  35823  cdlemefrs29bpre0  35824  cdlemefrs29cpre1  35826  cdleme32a  35869  cdlemftr3  35993  dvhopellsm  36546  dibelval3  36576  diblsmopel  36600  mapdvalc  37058  mapdval4N  37061  mapdordlem1a  37063