Theorem anass 631

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 20	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ph /\ ( ps /\ ch ) ) )
2	1	anassrs 630	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 20	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 629	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) /\ ch ) )
5	2, 4	impbii 181	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 177   /\ wa 359

This theorem is referenced by:  an12  773  an32  774  an13  775  an31  776  an4  798  3anass  940  4exdistrOLD  1931  2sb5  2161  2sb5rf  2167  sbel2x  2175  r2exf  2702  r19.41  2820  ceqsex3v  2954  ceqsrex2v  3031  rexrab  3058  rexrab2  3062  2reu5  3102  rexss  3370  inass  3511  indifdir  3557  difin2  3563  difrab  3575  reupick3  3586  inssdif0  3655  rexdifsn  3891  eqvinop  4401  copsexg  4402  wefrc  4536  uniuni  4675  reusv2lem4  4686  reusv2  4688  rabxp  4873  elvvv  4896  resopab2  5149  ssrnres  5268  elxp4  5316  elxp5  5317  cnvresima  5318  mptpreima  5322  coass  5347  imadif  5487  dff1o2  5638  eqfnfv3  5788  rexsupp  5814  isoini  6017  f1oiso  6030  oprabid  6064  dfoprab2  6080  mpt2eq123  6092  mpt2mptx  6123  resoprab2  6126  oprabex3  6147  ov3  6169  difxp  6339  frxp  6415  brtpos2  6444  oeeui  6804  oeeu  6805  omabs  6849  mapsnen  7143  xpsnen  7151  xpcomco  7157  xpassen  7161  wemapso2lem  7475  epfrs  7623  bnd2  7773  aceq1  7954  dfac5lem1  7960  dfac5lem2  7961  dfac5lem5  7964  kmlem3  7988  kmlem14  7999  pwfseqlem1  8489  ltexpi  8735  ltexprlem4  8872  axaddf  8976  axmulf  8977  rexuz  10483  rexuz2  10484  nnwos  10500  zmin  10526  rexrp  10587  elixx3g  10885  elfz2  11006  fzind2  11153  hashbclem  11656  resqrex  12011  rlim  12244  divalglem10  12877  divalgb  12879  gcdass  13000  isprm2  13042  infpn2  13236  ispos2  14360  issubg3  14915  resscntz  15085  subgdmdprd  15547  dprd2d2  15557  dfrhm2  15776  isassa  16330  aspval2  16360  istps2OLD  16941  istps3OLD  16942  ntreq0  17096  cmpcov2  17407  llyi  17490  nllyi  17491  subislly  17497  ptpjpre1  17556  tx1cn  17594  tx2cn  17595  txtube  17625  txkgen  17637  trfil2  17872  elflim2  17949  cnpflfi  17984  isfcls  17994  cnextcn  18051  istlm  18167  blres  18414  metrest  18507  isnlm  18664  elcncf1di  18878  elpi1  19023  iscph  19086  cfilucfil3OLD  19224  cfilucfil3  19225  itg1climres  19559  itgsubst  19886  ulmdvlem3  20271  cubic  20642  vmasum  20953  logfac2  20954  lgsquadlem1  21091  lgsquadlem2  21092  nb3grapr2  21416  trls  21489  3v3e3cycl2  21604  grpoidinvlem3  21747  h2hlm  22436  issh  22663  issh3  22675  ocsh  22738  cvbr2  23739  cvnbtwn2  23743  mdsl2i  23778  cvmdi  23780  mdsymlem2  23860  sumdmdii  23871  1stpreima  24048  2ndpreima  24049  1stmbfm  24563  2ndmbfm  24564  dya2iocnei  24585  iscvm  24899  axacprim  25109  dfpo2  25326  dfdm5  25346  dfrn5  25347  preduz  25414  wfi  25421  frind  25457  sltval2  25524  nofulllem5  25574  dfon3  25646  elfuns  25668  brimg  25690  brsuccf  25694  dfrdg4  25703  tfrqfree  25704  axcontlem5  25811  ifscgr  25882  cgrxfr  25893  segcon2  25943  seglecgr12im  25948  segletr  25952  ellines  25990  itg2addnc  26158  areacirclem6  26186  neifg  26290  isbnd2  26382  heibor1  26409  prtlem70  26588  prtlem100  26594  diophrex  26724  rmxdioph  26977  dford4  26990  islmodfg  27035  islssfg2  27037  isdomn3  27391  fgraphopab  27397  2sbc5g  27484  rexdifpr  27947  usgra2pth0  28042  usg2spthonot0  28086  usg2spthonot1  28087  1to2vfriswmgra  28110  usgreg2spot  28170  bnj250  28771  bnj251  28772  bnj256  28776  bnj168  28803  2sb5NEW7  29310  sbel2xNEW7  29315  2sb5rfOLD7  29446  lsateln0  29478  islshpat  29500  lcvbr2  29505  lcvnbtwn2  29510  isopos  29663  cvrval2  29757  cvrnbtwn2  29758  ishlat2  29836  3dim0  29939  islvol5  30061  pmapjat1  30335  pclcmpatN  30383  pclfinclN  30432  cdlemefrs29pre00  30877  cdlemefrs29bpre0  30878  cdlemefrs29cpre1  30880  cdleme32a  30923  cdlemftr3  31047  dvhopellsm  31600  dibelval3  31630  diblsmopel  31654  mapdvalc  32112  mapdval4N  32115  mapdordlem1a  32117

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361