Theorem anass 659

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

Syntax hints:   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  an12  811  an32  812  an13  813  an31  814  an4  838  3anass  995  3an4anass  1241  2sb5  2283  r2exfOLD  2924  r19.41v  2954  r19.41  2955  ceqsex3v  3100  ceqsrex2v  3186  rexrab  3214  rexrab2  3218  2reu5  3260  rexss  3508  inass  3654  indifdir  3711  difin2  3717  difrab  3729  reupick3  3740  inssdif0  3846  rexdifsn  4114  reusv2lem4  4621  reusv2  4623  eqvinop  4700  copsexg  4701  wefrc  4847  rabxp  4890  elvvv  4913  resopab2  5172  difxp  5280  ssrnres  5294  cnvresima  5343  mptpreima  5347  coass  5373  wfi  5432  imadif  5680  dff1o2  5842  eqfnfv3  6001  isoini  6254  f1oiso  6267  oprabid  6342  dfoprab2  6364  mpt2eq123  6377  mpt2mptx  6414  resoprab2  6420  ov3  6460  uniuni  6627  elxp4  6764  elxp5  6765  oprabex3  6809  frxp  6933  rexsupp  6960  brtpos2  7005  oeeui  7329  oeeu  7330  omabs  7374  mapsnen  7673  xpsnen  7682  xpcomco  7688  xpassen  7692  wemapsolem  8091  epfrs  8241  bnd2  8390  aceq1  8574  dfac5lem1  8580  dfac5lem2  8581  dfac5lem5  8584  kmlem3  8608  kmlem14  8619  pwfseqlem1  9109  ltexpi  9353  ltexprlem4  9490  axaddf  9595  axmulf  9596  rexuz  11238  rexuz2  11239  nnwos  11255  zmin  11289  rexrp  11351  elixx3g  11677  elfz2  11820  preduz  11942  fzind2  12054  hashbclem  12648  resqrex  13363  rlim  13608  divalglem10  14432  divalgb  14434  gcdass  14562  lcmass  14628  isprm2  14681  infpn2  14906  ispos2  16242  issubg3  16884  resscntz  17034  subgdmdprd  17716  dprd2d2  17726  dfrhm2  17994  isassa  18588  aspval2  18620  fvmptnn04if  19922  ntreq0  20142  cmpcov2  20454  llyi  20538  nllyi  20539  subislly  20545  ptpjpre1  20635  tx1cn  20673  tx2cn  20674  txtube  20704  txkgen  20716  trfil2  20951  elflim2  21028  cnpflfi  21063  isfcls  21073  cnextcn  21131  istlm  21248  blres  21495  metrest  21588  isnlm  21727  elcncf1di  21976  elpi1  22125  iscph  22197  cfilucfil3  22337  itg1climres  22721  itgsubst  23050  ulmdvlem3  23406  cubic  23824  vmasum  24193  logfac2  24194  lgsquadlem1  24331  lgsquadlem2  24332  legov  24679  ltgov  24691  perpln1  24804  axcontlem5  25047  nb3grapr2  25231  trls  25315  3v3e3cycl2  25441  wwlknprop  25463  wwlkextwrd  25505  wwlknfi  25515  wlknwwlknvbij  25517  isclwlk  25533  clwwlkvbij  25578  usg2spthonot0  25666  usg2spthonot1  25667  rusgranumwlkl1  25724  rusgranumwlklem3  25728  rusgra0edg  25732  1to2vfriswmgra  25783  usgreg2spot  25844  numclwwlkovf2  25861  grpoidinvlem3  25983  h2hlm  26682  issh  26910  issh3  26921  ocsh  26985  cvbr2  27985  cvnbtwn2  27989  mdsl2i  28024  cvmdi  28026  mdsymlem2  28106  sumdmdii  28117  spc2ed  28155  rabrab  28183  disjunsn  28253  mpt2mptxf  28329  1stpreima  28336  2ndpreima  28337  f1od2  28358  nndiffz1  28415  omndmul2  28524  smatrcl  28671  crefdf  28724  pcmplfin  28736  1stmbfm  29131  2ndmbfm  29132  dya2iocnei  29153  eulerpartlemgvv  29258  eulerpartlemn  29263  bnj250  29555  bnj251  29556  bnj256  29560  bnj168  29587  iscvm  30031  axacprim  30383  dfpo2  30444  dfdm5  30467  dfrn5  30468  elima4  30470  frind  30530  sltval2  30592  nofulllem5  30644  dfon3  30708  brimg  30753  dfrecs2  30766  dfrdg4  30767  ifscgr  30860  cgrxfr  30871  segcon2  30921  seglecgr12im  30926  segletr  30930  ellines  30968  neifg  31076  bj-dfmpt2a  31675  topdifinffinlem  31795  icorempt2  31799  finxpreclem6  31833  wl-cases2-dnf  31895  poimirlem26  32011  poimirlem28  32013  poimirlem30  32015  poimirlem32  32017  poimir  32018  itg2addnc  32041  ftc1anclem5  32066  ftc1anc  32070  areacirclem5  32081  isbnd2  32160  heibor1  32187  mergeconj  32383  prtlem70  32470  prtlem100  32474  lsateln0  32606  islshpat  32628  lcvbr2  32633  lcvnbtwn2  32638  isopos  32791  cvrval2  32885  cvrnbtwn2  32886  ishlat2  32964  3dim0  33067  islvol5  33189  pmapjat1  33463  pclcmpatN  33511  pclfinclN  33560  cdlemefrs29pre00  34007  cdlemefrs29bpre0  34008  cdlemefrs29cpre1  34010  cdleme32a  34053  cdlemftr3  34177  dvhopellsm  34730  dibelval3  34760  diblsmopel  34784  mapdvalc  35242  mapdval4N  35245  mapdordlem1a  35247  diophrex  35663  rmxdioph  35916  dford4  35929  islmodfg  35972  islssfg2  35974  isdomn3  36126  fgraphopab  36132  2sbc5g  36811  mapsnend  37518  limcrecl  37747  dvnmul  37856  dvnprodlem2  37860  fourierdlem83  38091  iundjiun  38336  rexdifpr  39034  nbgrel  39460  nbusgredgeu0  39492  nb3grpr2  39507  wlkOnwlk  39712  isclWlke  39804  usgra2pth0  39942  isrnghm  40165  isrnghmmul  40166  rngcinv  40256  rngcinvALTV  40268  ringcinv  40307  ringcinvALTV  40331  mpt2mptx2  40389