Theorem sylan9eqr 2154

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)

Hypotheses

Ref	Expression
sylan9eqr.1	|- ( ph -> A = B )
sylan9eqr.2	|- ( ps -> B = C )

Assertion

Ref	Expression
sylan9eqr	|- ( ( ps /\ ph ) -> A = C )

Proof of Theorem sylan9eqr

Step	Hyp	Ref	Expression
1		sylan9eqr.1	. . 3 |- ( ph -> A = B )
2		sylan9eqr.2	. . 3 |- ( ps -> B = C )
3	1, 2	sylan9eq 2152	. 2 |- ( ( ph /\ ps ) -> A = C )
4	3	ancoms 266	1 |- ( ( ps /\ ph ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  sbcied2  2898  csbied2  2997  fun2ssres  5102  fcoi1  5239  fcoi2  5240  funssfv  5379  caovimo  5896  mpomptsx  6025  dmmpossx  6027  fmpox  6028  2ndconst  6049  mpoxopoveq  6067  tfrlemisucaccv  6152  tfr1onlemsucaccv  6168  tfrcllemsucaccv  6181  rdgivallem  6208  nnmass  6313  nnm00  6355  ssenen  6674  exmidfodomrlemim  6966  ltexnqq  7117  ltrnqg  7129  nqnq0a  7163  nqnq0m  7164  nq0m0r  7165  nq0a0  7166  addnqprllem  7236  addnqprulem  7237  rereceu  7574  addid0  8002  nnnn0addcl  8859  zindd  9021  qaddcl  9277  qmulcl  9279  qreccl  9284  xaddpnf1  9470  xaddmnf1  9472  xaddnemnf  9481  xaddnepnf  9482  xaddcom  9485  xnegdi  9492  xaddass  9493  xpncan  9495  xleadd1a  9497  xltadd1  9500  xlt2add  9504  modfzo0difsn  10009  frec2uzrdg  10023  expp1  10141  expnegap0  10142  expcllem  10145  mulexp  10173  expmul  10179  sqoddm1div8  10285  bcpasc  10353  hashfzo  10409  shftfn  10437  reim0b  10475  cjexp  10506  sumsnf  11017  binomlem  11091  ef0lem  11164  dvdsnegb  11305  m1expe  11391  m1expo  11392  m1exp1  11393  flodddiv4  11426  gcdabs  11471  bezoutr1  11514  dvdslcm  11543  lcmeq0  11545  lcmcl  11546  lcmabs  11550  lcmgcdlem  11551  lcmdvds  11553  mulgcddvds  11568  qredeu  11571  divgcdcoprmex  11576  isxmet2d  12276  blfvalps  12313  blssioo  12464