Theorem anass 647

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

Syntax hints:   <-> wb 184   /\ wa 367

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 369

This theorem is referenced by:  an12  795  an32  796  an13  797  an31  798  an4  822  3anass  975  3an4anass  1217  2sb5  2189  r2exfOLD  2976  r19.41v  3006  r19.41  3007  ceqsex3v  3146  ceqsrex2v  3232  rexrab  3260  rexrab2  3264  2reu5  3305  rexss  3553  inass  3694  indifdir  3751  difin2  3757  difrab  3769  reupick3  3780  inssdif0  3883  rexdifsn  4145  reusv2lem4  4641  reusv2  4643  eqvinop  4721  copsexg  4722  wefrc  4862  rabxp  5025  elvvv  5048  resopab2  5310  difxp  5416  ssrnres  5430  cnvresima  5479  mptpreima  5483  coass  5509  imadif  5645  dff1o2  5803  eqfnfv3  5959  rexsuppOLD  5988  isoini  6209  f1oiso  6222  oprabid  6297  dfoprab2  6316  mpt2eq123  6329  mpt2mptx  6366  resoprab2  6372  ov3  6412  uniuni  6582  elxp4  6717  elxp5  6718  oprabex3  6762  frxp  6883  rexsupp  6910  brtpos2  6953  oeeui  7243  oeeu  7244  omabs  7288  mapsnen  7586  xpsnen  7594  xpcomco  7600  xpassen  7604  wemapsolem  7967  epfrs  8153  bnd2  8302  aceq1  8489  dfac5lem1  8495  dfac5lem2  8496  dfac5lem5  8499  kmlem3  8523  kmlem14  8534  pwfseqlem1  9025  ltexpi  9269  ltexprlem4  9406  axaddf  9511  axmulf  9512  rexuz  11132  rexuz2  11133  nnwos  11150  zmin  11179  rexrp  11241  elixx3g  11545  elfz2  11682  fzind2  11905  hashbclem  12488  resqrex  13169  rlim  13403  divalglem10  14147  divalgb  14149  gcdass  14270  isprm2  14312  infpn2  14518  ispos2  15779  issubg3  16421  resscntz  16571  subgdmdprd  17279  dprd2d2  17291  dfrhm2  17564  isassa  18162  aspval2  18194  fvmptnn04if  19520  istps2OLD  19592  istps3OLD  19593  ntreq0  19748  cmpcov2  20060  llyi  20144  nllyi  20145  subislly  20151  ptpjpre1  20241  tx1cn  20279  tx2cn  20280  txtube  20310  txkgen  20322  trfil2  20557  elflim2  20634  cnpflfi  20669  isfcls  20679  cnextcn  20736  istlm  20856  blres  21103  metrest  21196  isnlm  21353  elcncf1di  21568  elpi1  21714  iscph  21786  cfilucfil3OLD  21926  cfilucfil3  21927  itg1climres  22290  itgsubst  22619  ulmdvlem3  22966  cubic  23380  vmasum  23692  logfac2  23693  lgsquadlem1  23830  lgsquadlem2  23831  legov  24176  ltgov  24187  perpln1  24291  axcontlem5  24476  nb3grapr2  24659  trls  24743  3v3e3cycl2  24869  wwlknprop  24891  wwlkextwrd  24933  wwlknfi  24943  wlknwwlknvbij  24945  isclwlk  24961  clwwlkvbij  25006  usg2spthonot0  25094  usg2spthonot1  25095  rusgranumwlkl1  25152  rusgranumwlklem3  25156  rusgra0edg  25160  1to2vfriswmgra  25211  usgreg2spot  25272  numclwwlkovf2  25289  grpoidinvlem3  25409  h2hlm  26098  issh  26326  issh3  26338  ocsh  26402  cvbr2  27403  cvnbtwn2  27407  mdsl2i  27442  cvmdi  27444  mdsymlem2  27524  sumdmdii  27535  spc2ed  27573  rabrab  27600  disjunsn  27667  mpt2mptxf  27749  1stpreima  27756  2ndpreima  27757  f1od2  27781  nndiffz1  27833  omndmul2  27939  crefdf  28089  pcmplfin  28101  1stmbfm  28471  2ndmbfm  28472  dya2iocnei  28493  eulerpartlemgvv  28582  eulerpartlemn  28587  iscvm  28971  axacprim  29323  dfpo2  29428  dfdm5  29449  dfrn5  29450  elima4  29452  preduz  29523  wfi  29530  frind  29566  sltval2  29659  nofulllem5  29709  dfon3  29773  brimg  29818  brsuccf  29822  dfrdg4  29831  tfrqfree  29832  ifscgr  29925  cgrxfr  29936  segcon2  29986  seglecgr12im  29991  segletr  29995  ellines  30033  wl-cases2-dnf  30213  itg2addnc  30312  ftc1anclem5  30337  ftc1anc  30341  areacirclem5  30354  neifg  30432  isbnd2  30522  heibor1  30549  mergeconj  30745  prtlem70  30835  prtlem100  30839  diophrex  30951  rmxdioph  31200  dford4  31213  islmodfg  31257  islssfg2  31259  isdomn3  31408  fgraphopab  31414  lcmass  31462  2sbc5g  31567  limcrecl  31877  dvnmul  31982  dvnprodlem2  31986  fourierdlem83  32214  rexdifpr  32693  usgra2pth0  32746  isrnghm  32971  isrnghmmul  32972  rngcinv  33062  rngcinvALTV  33074  ringcinv  33113  ringcinvALTV  33137  mpt2mptx2  33197  bnj250  34173  bnj251  34174  bnj256  34178  bnj168  34205  lsateln0  35136  islshpat  35158  lcvbr2  35163  lcvnbtwn2  35168  isopos  35321  cvrval2  35415  cvrnbtwn2  35416  ishlat2  35494  3dim0  35597  islvol5  35719  pmapjat1  35993  pclcmpatN  36041  pclfinclN  36090  cdlemefrs29pre00  36537  cdlemefrs29bpre0  36538  cdlemefrs29cpre1  36540  cdleme32a  36583  cdlemftr3  36707  dvhopellsm  37260  dibelval3  37290  diblsmopel  37314  mapdvalc  37772  mapdval4N  37775  mapdordlem1a  37777