Theorem anass 398

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpan10  465  an12  550  an32  551  an13  552  an31  553  an4  575  3anass  966  sbidm  1823  4exdistr  1888  2sb5  1956  2sb5rf  1962  sbel2x  1971  r2exf  2451  r19.41  2584  ceqsex3v  2723  ceqsrex2v  2812  rexrab  2842  rexrab2  2846  rexss  3159  inass  3281  difin2  3333  difrab  3345  reupick3  3356  inssdif0im  3425  rexdifsn  3650  unidif0  4086  bnd2  4092  eqvinop  4160  copsexg  4161  uniuni  4367  rabxp  4571  elvvv  4597  rexiunxp  4676  resopab2  4861  ssrnres  4976  elxp4  5021  elxp5  5022  cnvresima  5023  mptpreima  5027  coass  5052  dff1o2  5365  eqfnfv3  5513  rexsupp  5537  isoini  5712  f1oiso  5720  oprabid  5796  dfoprab2  5811  mpoeq123  5823  mpomptx  5855  resoprab2  5861  ovi3  5900  oprabex3  6020  spc2ed  6123  f1od2  6125  brtpos2  6141  mapsnen  6698  xpsnen  6708  xpcomco  6713  xpassen  6717  ltexpi  7138  enq0enq  7232  enq0tr  7235  prnmaxl  7289  prnminu  7290  genpdflem  7308  ltexprlemm  7401  suplocsrlemb  7607  axaddf  7669  axmulf  7670  rexuz  9368  rexuz2  9369  rexrp  9457  elixx3g  9677  elfz2  9790  fzdifsuc  9854  fzind2  10009  divalgb  11611  gcdass  11692  lcmass  11755  isprm2  11787  ntreq0  12290  tx1cn  12427  tx2cn  12428  blres  12592  metrest  12664  elcncf1di  12724  dedekindicclemicc  12768