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  457  an12  525  an32  526  an13  527  an31  528  an4  550  3anass  923  sbidm  1772  4exdistr  1834  2sb5  1900  2sb5rf  1906  sbel2x  1915  r2exf  2384  r19.41  2509  ceqsex3v  2641  ceqsrex2v  2727  rexrab  2755  rexrab2  2759  rexss  3061  inass  3176  difin2  3226  difrab  3238  reupick3  3249  inssdif0im  3311  rexdifsn  3521  unidif0  3941  bnd2  3947  eqvinop  3998  copsexg  3999  uniuni  4201  rabxp  4398  elvvv  4421  rexiunxp  4496  resopab2  4675  ssrnres  4783  elxp4  4828  elxp5  4829  cnvresima  4830  mptpreima  4834  coass  4859  dff1o2  5151  eqfnfv3  5288  rexsupp  5312  isoini  5477  f1oiso  5485  oprabid  5557  dfoprab2  5572  mpt2eq123  5584  mpt2mptx  5615  resoprab2  5618  ovi3  5657  oprabex3  5776  spc2ed  5874  f1od2  5876  brtpos2  5889  xpsnen  6318  xpcomco  6323  xpassen  6327  ltexpi  6527  enq0enq  6621  enq0tr  6624  prnmaxl  6678  prnminu  6679  genpdflem  6697  ltexprlemm  6790  rexuz  8668  rexuz2  8669  rexrp  8756  elixx3g  8924  elfz2  9036  fzdifsuc  9098  fzind2  9248  divalgb  10325  gcdass  10404  lcmass  10467  isprm2  10499