Theorem anass 401

Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-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 19	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ph /\ ( ps /\ ch ) ) )
2	1	anassrs 400	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 19	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 399	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) /\ ch ) )
5	2, 4	impbii 126	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bianass  469  mpan10  474  an12  561  an32  562  an13  563  an31  564  an4  586  3anass  984  sbidm  1862  4exdistr  1928  2sb5  1999  2sb5rf  2005  sbel2x  2014  r2exf  2512  r19.41  2649  ceqsex3v  2802  ceqsrex2v  2892  rexrab  2923  rexrab2  2927  rexss  3246  inass  3369  difin2  3421  difrab  3433  reupick3  3444  inssdif0im  3514  rexdifpr  3646  rexdifsn  3750  unidif0  4196  bnd2  4202  eqvinop  4272  copsexg  4273  uniuni  4482  rabxp  4696  elvvv  4722  rexiunxp  4804  resopab2  4989  ssrnres  5108  elxp4  5153  elxp5  5154  cnvresima  5155  mptpreima  5159  coass  5184  dff1o2  5505  eqfnfv3  5657  rexsupp  5682  isoini  5861  f1oiso  5869  oprabid  5950  dfoprab2  5965  mpoeq123  5977  mpomptx  6009  resoprab2  6015  ovi3  6055  oprabex3  6181  spc2ed  6286  f1od2  6288  brtpos2  6304  mapsnen  6865  xpsnen  6875  xpcomco  6880  xpassen  6884  ltexpi  7397  enq0enq  7491  enq0tr  7494  prnmaxl  7548  prnminu  7549  genpdflem  7567  ltexprlemm  7660  suplocsrlemb  7866  axaddf  7928  axmulf  7929  rexuz  9645  rexuz2  9646  rexrp  9742  elixx3g  9967  elfz2  10081  fzdifsuc  10147  fzind2  10306  divalgb  12066  gcdass  12152  nnwosdc  12176  lcmass  12223  isprm2  12255  infpn2  12613  fngsum  12971  igsumvalx  12972  issubg3  13262  dfrhm2  13650  ntreq0  14300  tx1cn  14437  tx2cn  14438  blres  14602  metrest  14674  elcncf1di  14734  dedekindicclemicc  14786  lgsquadlem1  15191