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 23	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ph /\ ( ps /\ ch ) ) )
2	1	anassrs 652	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 23	. . 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  2239  r2exfOLD  2957  r19.41v  2987  r19.41  2988  ceqsex3v  3127  ceqsrex2v  3213  rexrab  3241  rexrab2  3245  2reu5  3286  rexss  3534  inass  3678  indifdir  3735  difin2  3741  difrab  3753  reupick3  3764  inssdif0  3868  rexdifsn  4132  reusv2lem4  4629  reusv2  4631  eqvinop  4706  copsexg  4707  wefrc  4848  rabxp  4891  elvvv  4914  resopab2  5173  difxp  5281  ssrnres  5295  cnvresima  5344  mptpreima  5348  coass  5374  wfi  5432  imadif  5676  dff1o2  5836  eqfnfv3  5993  isoini  6244  f1oiso  6257  oprabid  6332  dfoprab2  6351  mpt2eq123  6364  mpt2mptx  6401  resoprab2  6407  ov3  6447  uniuni  6614  elxp4  6751  elxp5  6752  oprabex3  6796  frxp  6917  rexsupp  6944  brtpos2  6987  oeeui  7311  oeeu  7312  omabs  7356  mapsnen  7654  xpsnen  7662  xpcomco  7668  xpassen  7672  wemapsolem  8065  epfrs  8214  bnd2  8363  aceq1  8546  dfac5lem1  8552  dfac5lem2  8553  dfac5lem5  8556  kmlem3  8580  kmlem14  8591  pwfseqlem1  9082  ltexpi  9326  ltexprlem4  9463  axaddf  9568  axmulf  9569  rexuz  11209  rexuz2  11210  nnwos  11226  zmin  11260  rexrp  11322  elixx3g  11648  elfz2  11789  preduz  11909  fzind2  12020  hashbclem  12610  resqrex  13293  rlim  13537  divalglem10  14358  divalgb  14360  gcdass  14484  lcmass  14550  isprm2  14603  infpn2  14820  ispos2  16144  issubg3  16786  resscntz  16936  subgdmdprd  17602  dprd2d2  17612  dfrhm2  17880  isassa  18474  aspval2  18506  fvmptnn04if  19804  ntreq0  20024  cmpcov2  20336  llyi  20420  nllyi  20421  subislly  20427  ptpjpre1  20517  tx1cn  20555  tx2cn  20556  txtube  20586  txkgen  20598  trfil2  20833  elflim2  20910  cnpflfi  20945  isfcls  20955  cnextcn  21013  istlm  21130  blres  21377  metrest  21470  isnlm  21609  elcncf1di  21823  elpi1  21969  iscph  22041  cfilucfil3  22181  itg1climres  22549  itgsubst  22878  ulmdvlem3  23222  cubic  23640  vmasum  24007  logfac2  24008  lgsquadlem1  24145  lgsquadlem2  24146  legov  24490  ltgov  24502  perpln1  24612  axcontlem5  24844  nb3grapr2  25027  trls  25111  3v3e3cycl2  25237  wwlknprop  25259  wwlkextwrd  25301  wwlknfi  25311  wlknwwlknvbij  25313  isclwlk  25329  clwwlkvbij  25374  usg2spthonot0  25462  usg2spthonot1  25463  rusgranumwlkl1  25520  rusgranumwlklem3  25524  rusgra0edg  25528  1to2vfriswmgra  25579  usgreg2spot  25640  numclwwlkovf2  25657  grpoidinvlem3  25779  h2hlm  26468  issh  26696  issh3  26707  ocsh  26771  cvbr2  27771  cvnbtwn2  27775  mdsl2i  27810  cvmdi  27812  mdsymlem2  27892  sumdmdii  27903  spc2ed  27941  rabrab  27970  disjunsn  28043  mpt2mptxf  28120  1stpreima  28127  2ndpreima  28128  f1od2  28152  nndiffz1  28202  omndmul2  28313  smatrcl  28461  crefdf  28514  pcmplfin  28526  1stmbfm  28921  2ndmbfm  28922  dya2iocnei  28943  eulerpartlemgvv  29035  eulerpartlemn  29040  bnj250  29294  bnj251  29295  bnj256  29299  bnj168  29326  iscvm  29770  axacprim  30122  dfpo2  30182  dfdm5  30205  dfrn5  30206  elima4  30208  frind  30268  sltval2  30330  nofulllem5  30380  dfon3  30444  brimg  30489  dfrecs2  30502  dfrdg4  30503  ifscgr  30596  cgrxfr  30607  segcon2  30657  seglecgr12im  30662  segletr  30666  ellines  30704  neifg  30812  topdifinffinlem  31484  icorempt2  31488  wl-cases2-dnf  31557  poimirlem26  31670  poimirlem28  31672  poimirlem30  31674  poimirlem32  31676  poimir  31677  itg2addnc  31700  ftc1anclem5  31725  ftc1anc  31729  areacirclem5  31740  isbnd2  31819  heibor1  31846  mergeconj  32042  prtlem70  32131  prtlem100  32135  lsateln0  32270  islshpat  32292  lcvbr2  32297  lcvnbtwn2  32302  isopos  32455  cvrval2  32549  cvrnbtwn2  32550  ishlat2  32628  3dim0  32731  islvol5  32853  pmapjat1  33127  pclcmpatN  33175  pclfinclN  33224  cdlemefrs29pre00  33671  cdlemefrs29bpre0  33672  cdlemefrs29cpre1  33674  cdleme32a  33717  cdlemftr3  33841  dvhopellsm  34394  dibelval3  34424  diblsmopel  34448  mapdvalc  34906  mapdval4N  34909  mapdordlem1a  34911  diophrex  35327  rmxdioph  35577  dford4  35590  islmodfg  35633  islssfg2  35635  isdomn3  35780  fgraphopab  35786  2sbc5g  36404  limcrecl  37281  dvnmul  37387  dvnprodlem2  37391  fourierdlem83  37621  iundjiun  37807  rexdifpr  38377  usgra2pth0  38425  isrnghm  38650  isrnghmmul  38651  rngcinv  38741  rngcinvALTV  38753  ringcinv  38792  ringcinvALTV  38816  mpt2mptx2  38876