Theorem sylan9eqr 2286

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 2284	. 2 |- ( ( ph /\ ps ) -> A = C )
4	3	ancoms 268	1 |- ( ( ps /\ ph ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  sbcied2  3069  csbied2  3175  fun2ssres  5370  fcoi1  5517  fcoi2  5518  funssfv  5665  caovimo  6216  mpomptsx  6362  dmmpossx  6364  fmpox  6365  2ndconst  6387  mpoxopoveq  6406  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  rdgivallem  6547  nnmass  6655  nnm00  6698  ssenen  7037  fi0  7174  nnnninf2  7326  nnnninfeq2  7328  exmidfodomrlemim  7412  ltexnqq  7628  ltrnqg  7640  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  nq0a0  7677  addnqprllem  7747  addnqprulem  7748  map2psrprg  8025  rereceu  8109  addid0  8552  nnnn0addcl  9432  zindd  9598  qaddcl  9869  qmulcl  9871  qreccl  9876  xaddpnf1  10081  xaddmnf1  10083  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xnegdi  10103  xaddass  10104  xpncan  10106  xleadd1a  10108  xltadd1  10111  xlt2add  10115  modfzo0difsn  10658  frec2uzrdg  10672  seqf1oglem2  10783  expp1  10809  expnegap0  10810  expcllem  10813  mulexp  10841  expmul  10847  sqoddm1div8  10956  bcpasc  11029  hashfzo  11087  lsw0  11165  ccatval1  11178  ccatval2  11179  swrdval  11233  ccatopth  11301  reuccatpfxs1  11332  shftfn  11402  reim0b  11440  cjexp  11471  sumsnf  11988  binomlem  12062  prodsnf  12171  ef0lem  12239  dvdsnegb  12387  m1expe  12478  m1expo  12479  m1exp1  12480  flodddiv4  12515  gcdabs  12577  bezoutr1  12622  dvdslcm  12659  lcmeq0  12661  lcmcl  12662  lcmabs  12666  lcmgcdlem  12667  lcmdvds  12669  mulgcddvds  12684  qredeu  12687  divgcdcoprmex  12692  pcge0  12904  pcgcd1  12919  pcadd  12931  pcmpt2  12935  mulgfvalg  13726  mulgnn0subcl  13740  mulgnn0z  13754  f1ghm0to0  13877  srgmulgass  14021  srgpcomp  14022  ringinvnzdiv  14082  lmodvsmmulgdi  14356  znval  14669  mplvalcoe  14723  isxmet2d  15091  blfvalps  15128  blssioo  15296  efper  15550  relogbcxpbap  15708  logbgcd1irr  15710  lgsdir  15783  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  lgsquadlem2  15826  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  wlklenvm1  16211  wlklenvm1g  16212  wlk0prc  16242  clwwlkn2  16291  trirec0xor  16700