Theorem anass 396

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 395	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 19	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 394	. 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpan10  463  an12  533  an32  534  an13  535  an31  536  an4  558  3anass  949  sbidm  1805  4exdistr  1868  2sb5  1934  2sb5rf  1940  sbel2x  1949  r2exf  2427  r19.41  2560  ceqsex3v  2699  ceqsrex2v  2787  rexrab  2816  rexrab2  2820  rexss  3130  inass  3252  difin2  3304  difrab  3316  reupick3  3327  inssdif0im  3396  rexdifsn  3621  unidif0  4051  bnd2  4057  eqvinop  4125  copsexg  4126  uniuni  4332  rabxp  4536  elvvv  4562  rexiunxp  4641  resopab2  4824  ssrnres  4939  elxp4  4984  elxp5  4985  cnvresima  4986  mptpreima  4990  coass  5015  dff1o2  5328  eqfnfv3  5474  rexsupp  5498  isoini  5673  f1oiso  5681  oprabid  5757  dfoprab2  5772  mpoeq123  5784  mpomptx  5816  resoprab2  5822  ovi3  5861  oprabex3  5981  spc2ed  6084  f1od2  6086  brtpos2  6102  mapsnen  6659  xpsnen  6668  xpcomco  6673  xpassen  6677  ltexpi  7090  enq0enq  7184  enq0tr  7187  prnmaxl  7241  prnminu  7242  genpdflem  7260  ltexprlemm  7353  axaddf  7600  axmulf  7601  rexuz  9274  rexuz2  9275  rexrp  9362  elixx3g  9574  elfz2  9687  fzdifsuc  9751  fzind2  9906  divalgb  11467  gcdass  11546  lcmass  11609  isprm2  11641  ntreq0  12141  tx1cn  12277  tx2cn  12278  blres  12420  metrest  12492  elcncf1di  12549