Theorem anass 399

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 398	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 19	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 397	. 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  466  an12  551  an32  552  an13  553  an31  554  an4  576  3anass  967  sbidm  1831  4exdistr  1896  2sb5  1963  2sb5rf  1969  sbel2x  1978  r2exf  2475  r19.41  2612  ceqsex3v  2754  ceqsrex2v  2844  rexrab  2875  rexrab2  2879  rexss  3195  inass  3317  difin2  3369  difrab  3381  reupick3  3392  inssdif0im  3461  rexdifpr  3588  rexdifsn  3691  unidif0  4128  bnd2  4134  eqvinop  4203  copsexg  4204  uniuni  4410  rabxp  4622  elvvv  4648  rexiunxp  4727  resopab2  4912  ssrnres  5027  elxp4  5072  elxp5  5073  cnvresima  5074  mptpreima  5078  coass  5103  dff1o2  5418  eqfnfv3  5566  rexsupp  5590  isoini  5765  f1oiso  5773  oprabid  5850  dfoprab2  5865  mpoeq123  5877  mpomptx  5909  resoprab2  5915  ovi3  5954  oprabex3  6074  spc2ed  6177  f1od2  6179  brtpos2  6195  mapsnen  6753  xpsnen  6763  xpcomco  6768  xpassen  6772  ltexpi  7251  enq0enq  7345  enq0tr  7348  prnmaxl  7402  prnminu  7403  genpdflem  7421  ltexprlemm  7514  suplocsrlemb  7720  axaddf  7782  axmulf  7783  rexuz  9485  rexuz2  9486  rexrp  9576  elixx3g  9798  elfz2  9912  fzdifsuc  9976  fzind2  10131  divalgb  11808  gcdass  11890  lcmass  11953  isprm2  11985  ntreq0  12503  tx1cn  12640  tx2cn  12641  blres  12805  metrest  12877  elcncf1di  12937  dedekindicclemicc  12981