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  820  3anass  969  2sb5  2158  2sb5rfOLD  2170  sbel2xOLD  2179  r2exf  2876  r19.41  2978  ceqsex3v  3118  ceqsrex2v  3202  rexrab  3230  rexrab2  3234  2reu5  3275  rexss  3528  inass  3669  indifdir  3715  difin2  3721  difrab  3733  reupick3  3744  inssdif0  3855  rexdifsn  4113  reusv2lem4  4605  reusv2  4607  eqvinop  4684  copsexg  4685  copsexgOLD  4686  wefrc  4823  rabxp  4984  elvvv  5007  resopab2  5264  difxp  5371  ssrnres  5385  cnvresima  5436  mptpreima  5440  coass  5465  imadif  5602  dff1o2  5755  eqfnfv3  5909  rexsuppOLD  5938  isoini  6139  f1oiso  6152  oprabid  6225  dfoprab2  6243  mpt2eq123  6255  mpt2mptx  6292  resoprab2  6298  ov3  6338  uniuni  6496  elxp4  6633  elxp5  6634  oprabex3  6677  frxp  6793  rexsupp  6818  brtpos2  6862  oeeui  7152  oeeu  7153  omabs  7197  mapsnen  7498  xpsnen  7506  xpcomco  7512  xpassen  7516  wemapsolem  7876  epfrs  8063  bnd2  8212  aceq1  8399  dfac5lem1  8405  dfac5lem2  8406  dfac5lem5  8409  kmlem3  8433  kmlem14  8444  pwfseqlem1  8937  ltexpi  9183  ltexprlem4  9320  axaddf  9424  axmulf  9425  rexuz  11017  rexuz2  11018  nnwos  11034  zmin  11061  rexrp  11122  elixx3g  11425  elfz2  11562  fzind2  11755  hashbclem  12324  resqrex  12859  rlim  13092  divalglem10  13725  divalgb  13727  gcdass  13848  isprm2  13890  infpn2  14093  ispos2  15238  issubg3  15819  resscntz  15969  subgdmdprd  16654  dprd2d2  16666  dfrhm2  16932  isassa  17511  aspval2  17541  istps2OLD  18659  istps3OLD  18660  ntreq0  18814  cmpcov2  19126  llyi  19211  nllyi  19212  subislly  19218  ptpjpre1  19277  tx1cn  19315  tx2cn  19316  txtube  19346  txkgen  19358  trfil2  19593  elflim2  19670  cnpflfi  19705  isfcls  19715  cnextcn  19772  istlm  19892  blres  20139  metrest  20232  isnlm  20389  elcncf1di  20604  elpi1  20750  iscph  20822  cfilucfil3OLD  20962  cfilucfil3  20963  itg1climres  21326  itgsubst  21655  ulmdvlem3  22001  cubic  22378  vmasum  22689  logfac2  22690  lgsquadlem1  22827  lgsquadlem2  22828  legov  23155  perpln1  23247  axcontlem5  23367  nb3grapr2  23515  trls  23588  3v3e3cycl2  23703  grpoidinvlem3  23846  h2hlm  24535  issh  24763  issh3  24775  ocsh  24839  cvbr2  25840  cvnbtwn2  25844  mdsl2i  25879  cvmdi  25881  mdsymlem2  25961  sumdmdii  25972  spc2ed  26010  rabrab  26037  disjunsn  26088  mpt2mptxf  26147  1stpreima  26153  2ndpreima  26154  f1od2  26176  nndiffz1  26221  1stmbfm  26820  2ndmbfm  26821  dya2iocnei  26842  eulerpartlemgvv  26904  eulerpartlemn  26909  iscvm  27293  axacprim  27503  dfpo2  27710  dfdm5  27732  dfrn5  27733  elima4  27735  preduz  27806  wfi  27813  frind  27849  sltval2  27942  nofulllem5  27992  dfon3  28068  brimg  28113  brsuccf  28117  dfrdg4  28126  tfrqfree  28127  ifscgr  28220  cgrxfr  28231  segcon2  28281  seglecgr12im  28286  segletr  28290  ellines  28328  itg2addnc  28595  ftc1anclem5  28620  ftc1anc  28624  areacirclem5  28637  neifg  28741  isbnd2  28831  heibor1  28858  mergeconj  29054  prtlem70  29145  prtlem100  29149  diophrex  29263  rmxdioph  29514  dford4  29527  islmodfg  29571  islssfg2  29573  isdomn3  29721  fgraphopab  29727  2sbc5g  29819  3an4anass  30264  rexdifpr  30273  usgra2pth0  30451  wwlknprop  30469  wwlkextwrd  30509  wwlknfi  30519  wlknwwlknvbij  30521  usg2spthonot0  30557  usg2spthonot1  30558  isclwlk  30570  clwwlkvbij  30612  rusgranumwlkl1  30708  rusgranumwlklem3  30718  rusgra0edg  30722  1to2vfriswmgra  30747  usgreg2spot  30809  numclwwlkovf2  30826  mpt2mptx2  30873  fvmptnn04if  31336  bnj250  32022  bnj251  32023  bnj256  32027  bnj168  32054  lsateln0  32979  islshpat  33001  lcvbr2  33006  lcvnbtwn2  33011  isopos  33164  cvrval2  33258  cvrnbtwn2  33259  ishlat2  33337  3dim0  33440  islvol5  33562  pmapjat1  33836  pclcmpatN  33884  pclfinclN  33933  cdlemefrs29pre00  34378  cdlemefrs29bpre0  34379  cdlemefrs29cpre1  34381  cdleme32a  34424  cdlemftr3  34548  dvhopellsm  35101  dibelval3  35131  diblsmopel  35155  mapdvalc  35613  mapdval4N  35616  mapdordlem1a  35618