Theorem anass 393

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpan10  458  an12  528  an32  529  an13  530  an31  531  an4  553  3anass  928  sbidm  1779  4exdistr  1841  2sb5  1907  2sb5rf  1913  sbel2x  1922  r2exf  2396  r19.41  2522  ceqsex3v  2661  ceqsrex2v  2747  rexrab  2776  rexrab2  2780  rexss  3086  inass  3208  difin2  3259  difrab  3271  reupick3  3282  inssdif0im  3347  rexdifsn  3567  unidif0  3994  bnd2  4000  eqvinop  4061  copsexg  4062  uniuni  4264  rabxp  4463  elvvv  4489  rexiunxp  4566  resopab2  4746  ssrnres  4860  elxp4  4905  elxp5  4906  cnvresima  4907  mptpreima  4911  coass  4936  dff1o2  5242  eqfnfv3  5383  rexsupp  5407  isoini  5579  f1oiso  5587  oprabid  5663  dfoprab2  5678  mpt2eq123  5690  mpt2mptx  5721  resoprab2  5724  ovi3  5763  oprabex3  5882  spc2ed  5980  f1od2  5982  brtpos2  5998  mapsnen  6508  xpsnen  6517  xpcomco  6522  xpassen  6526  ltexpi  6875  enq0enq  6969  enq0tr  6972  prnmaxl  7026  prnminu  7027  genpdflem  7045  ltexprlemm  7138  rexuz  9037  rexuz2  9038  rexrp  9125  elixx3g  9288  elfz2  9400  fzdifsuc  9462  fzind2  9615  divalgb  11018  gcdass  11097  lcmass  11160  isprm2  11192