Theorem anass 630

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 629	. 2 |- (((ph /\ ps) /\ ch) -> (ph /\ (ps /\ ch)))
3		id 19	. . 3 |- (((ph /\ ps) /\ ch) -> ((ph /\ ps) /\ ch))
4	3	anasss 628	. 2 |- ((ph /\ (ps /\ ch)) -> ((ph /\ ps) /\ ch))
5	2, 4	impbii 180	1 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:   <-> wb 176   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  an12  772  an32  773  an13  774  an31  775  an4  797  3anass  938  4exdistr  1911  2sb5  2112  2sb5rf  2117  sbel2x  2125  r2exf  2651  r19.41  2764  ceqsex3v  2898  ceqsrex2v  2975  rexrab  3001  rexrab2  3005  2reu5  3045  rexss  3334  inass  3466  indifdir  3512  difin2  3517  difrab  3530  reupick3  3541  inssdif0  3618  rexdifsn  3844  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  dfnnc2  4396  addcass  4416  copsexg  4608  setconslem1  4732  setconslem6  4737  rabxp  4815  brres  4950  resopab2  5002  ssrnres  5060  cnvresima  5078  coass  5098  elxp4  5109  fncnv  5159  imadif  5172  dff1o2  5292  eqfnfv3  5395  isoini  5498  f1oiso  5500  oprabid  5551  resoprab2  5583  fnov  5592  ov3  5600  mpt2eq123  5662  mptpreima  5683  mpt2mptx  5709  restxp  5787  brimage  5794  txpcofun  5804  addcfnex  5825  brpprod  5840  clos1induct  5881  frds  5936  lecex  6116  ceexlem1  6174  tcfnex  6245  nmembers1lem3  6271  nncdiv3lem1  6276  nchoicelem11  6300  nchoicelem16  6305