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  2650  r19.41  2763  ceqsex3v  2897  ceqsrex2v  2974  rexrab  3000  rexrab2  3004  2reu5  3044  rexss  3333  inass  3465  indifdir  3511  difin2  3516  difrab  3529  reupick3  3540  inssdif0  3617  rexdifsn  3843  opkelopkabg  4245  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  dfnnc2  4395  addcass  4415  copsexg  4607  setconslem1  4731  setconslem6  4736  rabxp  4814  brres  4949  resopab2  5001  ssrnres  5059  cnvresima  5077  coass  5097  elxp4  5108  fncnv  5158  imadif  5171  dff1o2  5291  eqfnfv3  5394  isoini  5497  f1oiso  5499  oprabid  5550  resoprab2  5582  fnov  5591  ov3  5599  mpt2eq123  5661  mptpreima  5682  mpt2mptx  5708  restxp  5786  brimage  5793  txpcofun  5803  addcfnex  5824  brpprod  5839  clos1induct  5880  frds  5935  lecex  6115  ceexlem1  6173  tcfnex  6244  nmembers1lem3  6270  nncdiv3lem1  6275  nchoicelem11  6299  nchoicelem16  6304