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  820  3anass  969  2sb5  2149  2sb5rfOLD  2161  sbel2xOLD  2170  r2exf  2746  r19.41  2867  ceqsex3v  3007  ceqsrex2v  3090  rexrab  3118  rexrab2  3122  2reu5  3162  rexss  3414  inass  3555  indifdir  3601  difin2  3607  difrab  3619  reupick3  3630  inssdif0  3741  rexdifsn  3999  reusv2lem4  4491  reusv2  4493  eqvinop  4570  copsexg  4571  copsexgOLD  4572  wefrc  4709  rabxp  4870  elvvv  4893  resopab2  5150  difxp  5257  ssrnres  5271  cnvresima  5322  mptpreima  5326  coass  5351  imadif  5488  dff1o2  5641  eqfnfv3  5794  rexsuppOLD  5823  isoini  6024  f1oiso  6037  oprabid  6110  dfoprab2  6128  mpt2eq123  6140  mpt2mptx  6176  resoprab2  6182  ov3  6222  uniuni  6380  elxp4  6517  elxp5  6518  oprabex3  6561  frxp  6677  rexsupp  6702  brtpos2  6746  oeeui  7033  oeeu  7034  omabs  7078  mapsnen  7379  xpsnen  7387  xpcomco  7393  xpassen  7397  wemapsolem  7756  epfrs  7943  bnd2  8092  aceq1  8279  dfac5lem1  8285  dfac5lem2  8286  dfac5lem5  8289  kmlem3  8313  kmlem14  8324  pwfseqlem1  8817  ltexpi  9063  ltexprlem4  9200  axaddf  9304  axmulf  9305  rexuz  10897  rexuz2  10898  nnwos  10914  zmin  10941  rexrp  11002  elixx3g  11305  elfz2  11436  fzind2  11629  hashbclem  12197  resqrex  12732  rlim  12965  divalglem10  13598  divalgb  13600  gcdass  13721  isprm2  13763  infpn2  13966  ispos2  15110  issubg3  15690  resscntz  15840  subgdmdprd  16519  dprd2d2  16531  dfrhm2  16796  isassa  17364  aspval2  17394  istps2OLD  18501  istps3OLD  18502  ntreq0  18656  cmpcov2  18968  llyi  19053  nllyi  19054  subislly  19060  ptpjpre1  19119  tx1cn  19157  tx2cn  19158  txtube  19188  txkgen  19200  trfil2  19435  elflim2  19512  cnpflfi  19547  isfcls  19557  cnextcn  19614  istlm  19734  blres  19981  metrest  20074  isnlm  20231  elcncf1di  20446  elpi1  20592  iscph  20664  cfilucfil3OLD  20804  cfilucfil3  20805  itg1climres  21167  itgsubst  21496  ulmdvlem3  21842  cubic  22219  vmasum  22530  logfac2  22531  lgsquadlem1  22668  lgsquadlem2  22669  legov  22987  axcontlem5  23165  nb3grapr2  23313  trls  23386  3v3e3cycl2  23501  grpoidinvlem3  23644  h2hlm  24333  issh  24561  issh3  24573  ocsh  24637  cvbr2  25638  cvnbtwn2  25642  mdsl2i  25677  cvmdi  25679  mdsymlem2  25759  sumdmdii  25770  spc2ed  25808  rabrab  25835  disjunsn  25887  mpt2mptxf  25946  1stpreima  25952  2ndpreima  25953  f1od2  25975  nndiffz1  26026  1stmbfm  26627  2ndmbfm  26628  dya2iocnei  26649  eulerpartlemgvv  26711  eulerpartlemn  26716  iscvm  27100  axacprim  27309  dfpo2  27516  dfdm5  27538  dfrn5  27539  elima4  27541  preduz  27612  wfi  27619  frind  27655  sltval2  27748  nofulllem5  27798  dfon3  27874  brimg  27919  brsuccf  27923  dfrdg4  27932  tfrqfree  27933  ifscgr  28026  cgrxfr  28037  segcon2  28087  seglecgr12im  28092  segletr  28096  ellines  28134  wl-lem-mo-recur  28346  itg2addnc  28399  ftc1anclem5  28424  ftc1anc  28428  areacirclem5  28441  neifg  28545  isbnd2  28635  heibor1  28662  mergeconj  28858  prtlem70  28949  prtlem100  28953  diophrex  29067  rmxdioph  29318  dford4  29331  islmodfg  29375  islssfg2  29377  isdomn3  29525  fgraphopab  29531  2sbc5g  29623  3an4anass  30068  rexdifpr  30077  usgra2pth0  30255  wwlknprop  30273  wwlkextwrd  30313  wwlknfi  30323  wlknwwlknvbij  30325  usg2spthonot0  30361  usg2spthonot1  30362  isclwlk  30374  clwwlkvbij  30416  rusgranumwlkl1  30512  rusgranumwlklem3  30522  rusgra0edg  30526  1to2vfriswmgra  30551  usgreg2spot  30613  numclwwlkovf2  30630  mpt2mptx2  30676  bnj250  31576  bnj251  31577  bnj256  31581  bnj168  31608  lsateln0  32480  islshpat  32502  lcvbr2  32507  lcvnbtwn2  32512  isopos  32665  cvrval2  32759  cvrnbtwn2  32760  ishlat2  32838  3dim0  32941  islvol5  33063  pmapjat1  33337  pclcmpatN  33385  pclfinclN  33434  cdlemefrs29pre00  33879  cdlemefrs29bpre0  33880  cdlemefrs29cpre1  33882  cdleme32a  33925  cdlemftr3  34049  dvhopellsm  34602  dibelval3  34632  diblsmopel  34656  mapdvalc  35114  mapdval4N  35117  mapdordlem1a  35119