Theorem anass 653

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

Syntax hints:   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  an12  804  an32  805  an13  806  an31  807  an4  831  3anass  986  3an4anass  1229  2sb5  2243  r2exfOLD  2883  r19.41v  2913  r19.41  2914  ceqsex3v  3057  ceqsrex2v  3142  rexrab  3170  rexrab2  3174  2reu5  3216  rexss  3464  inass  3608  indifdir  3665  difin2  3671  difrab  3683  reupick3  3694  inssdif0  3800  rexdifsn  4065  reusv2lem4  4564  reusv2  4566  eqvinop  4641  copsexg  4642  wefrc  4783  rabxp  4826  elvvv  4849  resopab2  5108  difxp  5216  ssrnres  5230  cnvresima  5279  mptpreima  5283  coass  5309  wfi  5368  imadif  5612  dff1o2  5772  eqfnfv3  5930  isoini  6181  f1oiso  6194  oprabid  6269  dfoprab2  6288  mpt2eq123  6301  mpt2mptx  6338  resoprab2  6344  ov3  6384  uniuni  6551  elxp4  6688  elxp5  6689  oprabex3  6733  frxp  6854  rexsupp  6881  brtpos2  6927  oeeui  7251  oeeu  7252  omabs  7296  mapsnen  7594  xpsnen  7602  xpcomco  7608  xpassen  7612  wemapsolem  8011  epfrs  8160  bnd2  8309  aceq1  8492  dfac5lem1  8498  dfac5lem2  8499  dfac5lem5  8502  kmlem3  8526  kmlem14  8537  pwfseqlem1  9027  ltexpi  9271  ltexprlem4  9408  axaddf  9513  axmulf  9514  rexuz  11153  rexuz2  11154  nnwos  11170  zmin  11204  rexrp  11266  elixx3g  11592  elfz2  11735  preduz  11855  fzind2  11966  hashbclem  12556  resqrex  13251  rlim  13495  divalglem10  14319  divalgb  14321  gcdass  14449  lcmass  14515  isprm2  14568  infpn2  14793  ispos2  16129  issubg3  16771  resscntz  16921  subgdmdprd  17603  dprd2d2  17613  dfrhm2  17881  isassa  18475  aspval2  18507  fvmptnn04if  19808  ntreq0  20028  cmpcov2  20340  llyi  20424  nllyi  20425  subislly  20431  ptpjpre1  20521  tx1cn  20559  tx2cn  20560  txtube  20590  txkgen  20602  trfil2  20837  elflim2  20914  cnpflfi  20949  isfcls  20959  cnextcn  21017  istlm  21134  blres  21381  metrest  21474  isnlm  21613  elcncf1di  21862  elpi1  22011  iscph  22083  cfilucfil3  22223  itg1climres  22607  itgsubst  22936  ulmdvlem3  23292  cubic  23710  vmasum  24079  logfac2  24080  lgsquadlem1  24217  lgsquadlem2  24218  legov  24565  ltgov  24577  perpln1  24690  axcontlem5  24933  nb3grapr2  25117  trls  25201  3v3e3cycl2  25327  wwlknprop  25349  wwlkextwrd  25391  wwlknfi  25401  wlknwwlknvbij  25403  isclwlk  25419  clwwlkvbij  25464  usg2spthonot0  25552  usg2spthonot1  25553  rusgranumwlkl1  25610  rusgranumwlklem3  25614  rusgra0edg  25618  1to2vfriswmgra  25669  usgreg2spot  25730  numclwwlkovf2  25747  grpoidinvlem3  25869  h2hlm  26568  issh  26796  issh3  26807  ocsh  26871  cvbr2  27871  cvnbtwn2  27875  mdsl2i  27910  cvmdi  27912  mdsymlem2  27992  sumdmdii  28003  spc2ed  28041  rabrab  28070  disjunsn  28143  mpt2mptxf  28219  1stpreima  28226  2ndpreima  28227  f1od2  28252  nndiffz1  28309  omndmul2  28419  smatrcl  28567  crefdf  28620  pcmplfin  28632  1stmbfm  29027  2ndmbfm  29028  dya2iocnei  29049  eulerpartlemgvv  29154  eulerpartlemn  29159  bnj250  29451  bnj251  29452  bnj256  29456  bnj168  29483  iscvm  29927  axacprim  30279  dfpo2  30339  dfdm5  30362  dfrn5  30363  elima4  30365  frind  30425  sltval2  30487  nofulllem5  30537  dfon3  30601  brimg  30646  dfrecs2  30659  dfrdg4  30660  ifscgr  30753  cgrxfr  30764  segcon2  30814  seglecgr12im  30819  segletr  30823  ellines  30861  neifg  30969  topdifinffinlem  31651  icorempt2  31655  finxpreclem6  31689  wl-cases2-dnf  31751  poimirlem26  31867  poimirlem28  31869  poimirlem30  31871  poimirlem32  31873  poimir  31874  itg2addnc  31897  ftc1anclem5  31922  ftc1anc  31926  areacirclem5  31937  isbnd2  32016  heibor1  32043  mergeconj  32239  prtlem70  32328  prtlem100  32332  lsateln0  32467  islshpat  32489  lcvbr2  32494  lcvnbtwn2  32499  isopos  32652  cvrval2  32746  cvrnbtwn2  32747  ishlat2  32825  3dim0  32928  islvol5  33050  pmapjat1  33324  pclcmpatN  33372  pclfinclN  33421  cdlemefrs29pre00  33868  cdlemefrs29bpre0  33869  cdlemefrs29cpre1  33871  cdleme32a  33914  cdlemftr3  34038  dvhopellsm  34591  dibelval3  34621  diblsmopel  34645  mapdvalc  35103  mapdval4N  35106  mapdordlem1a  35108  diophrex  35524  rmxdioph  35778  dford4  35791  islmodfg  35834  islssfg2  35836  isdomn3  35988  fgraphopab  35994  2sbc5g  36674  limcrecl  37586  dvnmul  37695  dvnprodlem2  37699  fourierdlem83  37930  iundjiun  38143  rexdifpr  38797  nbgrel  39140  nbusgredgeu0  39172  nb3grpr2  39182  usgra2pth0  39254  isrnghm  39477  isrnghmmul  39478  rngcinv  39568  rngcinvALTV  39580  ringcinv  39619  ringcinvALTV  39643  mpt2mptx2  39703