Theorem anass 649

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

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

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 371

This theorem is referenced by:  an12  795  an32  796  an13  797  an31  798  an4  822  3anass  977  3an4anass  1219  2sb5  2171  2sb5rfOLD  2183  sbel2xOLD  2192  r2exfOLD  2984  r19.41  3013  ceqsex3v  3153  ceqsrex2v  3239  rexrab  3267  rexrab2  3271  2reu5  3312  rexss  3567  inass  3708  indifdir  3754  difin2  3760  difrab  3772  reupick3  3783  inssdif0  3894  rexdifsn  4156  reusv2lem4  4651  reusv2  4653  eqvinop  4731  copsexg  4732  copsexgOLD  4733  wefrc  4873  rabxp  5035  elvvv  5058  resopab2  5320  difxp  5429  ssrnres  5443  cnvresima  5494  mptpreima  5498  coass  5524  imadif  5661  dff1o2  5819  eqfnfv3  5975  rexsuppOLD  6004  isoini  6220  f1oiso  6233  oprabid  6306  dfoprab2  6325  mpt2eq123  6338  mpt2mptx  6375  resoprab2  6381  ov3  6421  uniuni  6587  elxp4  6725  elxp5  6726  oprabex3  6770  frxp  6890  rexsupp  6915  brtpos2  6958  oeeui  7248  oeeu  7249  omabs  7293  mapsnen  7590  xpsnen  7598  xpcomco  7604  xpassen  7608  wemapsolem  7971  epfrs  8158  bnd2  8307  aceq1  8494  dfac5lem1  8500  dfac5lem2  8501  dfac5lem5  8504  kmlem3  8528  kmlem14  8539  pwfseqlem1  9032  ltexpi  9276  ltexprlem4  9413  axaddf  9518  axmulf  9519  rexuz  11127  rexuz2  11128  nnwos  11145  zmin  11174  rexrp  11235  elixx3g  11538  elfz2  11675  fzind2  11888  hashbclem  12463  resqrex  13043  rlim  13277  divalglem10  13915  divalgb  13917  gcdass  14038  isprm2  14080  infpn2  14286  ispos2  15431  issubg3  16014  resscntz  16164  subgdmdprd  16871  dprd2d2  16883  dfrhm2  17150  isassa  17735  aspval2  17767  fvmptnn04if  19117  istps2OLD  19189  istps3OLD  19190  ntreq0  19344  cmpcov2  19656  llyi  19741  nllyi  19742  subislly  19748  ptpjpre1  19807  tx1cn  19845  tx2cn  19846  txtube  19876  txkgen  19888  trfil2  20123  elflim2  20200  cnpflfi  20235  isfcls  20245  cnextcn  20302  istlm  20422  blres  20669  metrest  20762  isnlm  20919  elcncf1di  21134  elpi1  21280  iscph  21352  cfilucfil3OLD  21492  cfilucfil3  21493  itg1climres  21856  itgsubst  22185  ulmdvlem3  22531  cubic  22908  vmasum  23219  logfac2  23220  lgsquadlem1  23357  lgsquadlem2  23358  legov  23699  ltgov  23710  perpln1  23795  axcontlem5  23947  nb3grapr2  24130  trls  24214  3v3e3cycl2  24340  wwlknprop  24362  wwlkextwrd  24404  wwlknfi  24414  wlknwwlknvbij  24416  isclwlk  24432  clwwlkvbij  24477  usg2spthonot0  24565  usg2spthonot1  24566  rusgranumwlkl1  24623  rusgranumwlklem3  24627  rusgra0edg  24631  1to2vfriswmgra  24682  usgreg2spot  24744  numclwwlkovf2  24761  grpoidinvlem3  24884  h2hlm  25573  issh  25801  issh3  25813  ocsh  25877  cvbr2  26878  cvnbtwn2  26882  mdsl2i  26917  cvmdi  26919  mdsymlem2  26999  sumdmdii  27010  spc2ed  27048  rabrab  27075  disjunsn  27126  mpt2mptxf  27190  1stpreima  27196  2ndpreima  27197  f1od2  27219  nndiffz1  27264  1stmbfm  27871  2ndmbfm  27872  dya2iocnei  27893  eulerpartlemgvv  27955  eulerpartlemn  27960  iscvm  28344  axacprim  28554  dfpo2  28761  dfdm5  28783  dfrn5  28784  elima4  28786  preduz  28857  wfi  28864  frind  28900  sltval2  28993  nofulllem5  29043  dfon3  29119  brimg  29164  brsuccf  29168  dfrdg4  29177  tfrqfree  29178  ifscgr  29271  cgrxfr  29282  segcon2  29332  seglecgr12im  29337  segletr  29341  ellines  29379  itg2addnc  29646  ftc1anclem5  29671  ftc1anc  29675  areacirclem5  29688  neifg  29792  isbnd2  29882  heibor1  29909  mergeconj  30105  prtlem70  30196  prtlem100  30200  diophrex  30313  rmxdioph  30562  dford4  30575  islmodfg  30619  islssfg2  30621  isdomn3  30769  fgraphopab  30775  lcmass  30818  2sbc5g  30901  limcrecl  31171  fourierdlem83  31490  rexdifpr  31767  usgra2pth0  31824  mpt2mptx2  31988  bnj250  32833  bnj251  32834  bnj256  32838  bnj168  32865  lsateln0  33792  islshpat  33814  lcvbr2  33819  lcvnbtwn2  33824  isopos  33977  cvrval2  34071  cvrnbtwn2  34072  ishlat2  34150  3dim0  34253  islvol5  34375  pmapjat1  34649  pclcmpatN  34697  pclfinclN  34746  cdlemefrs29pre00  35191  cdlemefrs29bpre0  35192  cdlemefrs29cpre1  35194  cdleme32a  35237  cdlemftr3  35361  dvhopellsm  35914  dibelval3  35944  diblsmopel  35968  mapdvalc  36426  mapdval4N  36429  mapdordlem1a  36431