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  563  an32  564  an13  565  an31  566  an4  588  3anass  1009  sbidm  1900  4exdistr  1968  2sb5  2039  2sb5rf  2045  sbel2x  2054  r2exf  2562  r19.41  2700  ceqsex3v  2859  ceqsrex2v  2951  rexrab  2982  rexrab2  2986  rexss  3307  inass  3433  difin2  3485  difrab  3497  reupick3  3508  inssdif0im  3578  rexdifpr  3719  rexdifsn  3827  unidif0  4282  bnd2  4288  eqvinop  4361  copsexg  4362  uniuni  4574  rabxp  4789  elvvv  4815  rexiunxp  4899  resopab2  5087  ssrnres  5207  elxp4  5252  elxp5  5253  cnvresima  5254  mptpreima  5258  coass  5283  dff1o2  5621  eqfnfv3  5779  isoini  5993  f1oiso  6001  oprabid  6084  dfoprab2  6102  mpoeq123  6114  mpomptx  6146  resoprab2  6152  ovi3  6193  oprabex3  6324  spc2ed  6431  f1od2  6433  rexsupp  6455  brtpos2  6484  mapsnend  7054  mapsnen  7055  xpsnen  7074  xpcomco  7079  xpassen  7083  ltexpi  7654  enq0enq  7748  enq0tr  7751  prnmaxl  7805  prnminu  7806  genpdflem  7824  ltexprlemm  7917  suplocsrlemb  8123  axaddf  8185  axmulf  8186  rexuz  9915  rexuz2  9916  rexrp  10012  elixx3g  10237  elfz2  10352  fzdifsuc  10419  fzind2  10589  sseqn  11207  hashfibclem  11210  divalgb  12615  gcdass  12715  nnwosdc  12739  lcmass  12786  isprm2  12818  infpn2  13224  fngsum  13618  igsumvalx  13619  issubg3  13926  dfrhm2  14316  ntreq0  15014  tx1cn  15151  tx2cn  15152  blres  15316  metrest  15388  elcncf1di  15461  dedekindicclemicc  15514  fsumdvdsmul  15876  lgsquadlem1  15967  lgsquadlem2  15968  wlk1walkdom  16371  isclwwlk  16406  isclwwlknx  16428  clwwlknonel  16444  clwwlknon2x  16447  iseupthf1o  16460