Theorem sylan9eqr 2287

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  sbcied2  3080  csbied2  3186  fun2ssres  5396  fcoi1  5547  fcoi2  5548  funssfv  5696  caovimo  6248  mpomptsx  6393  dmmpossx  6395  fmpox  6396  2ndconst  6418  mpoxopoveq  6471  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  rdgivallem  6612  nnmass  6720  nnm00  6763  mapsnend  7052  ssenen  7105  fi0  7262  nnnninf2  7418  nnnninfeq2  7420  exmidfodomrlemim  7504  ltexnqq  7723  ltrnqg  7735  nqnq0a  7769  nqnq0m  7770  nq0m0r  7771  nq0a0  7772  addnqprllem  7842  addnqprulem  7843  map2psrprg  8120  rereceu  8204  addid0  8646  nnnn0addcl  9526  zindd  9696  qaddcl  9967  qmulcl  9969  qreccl  9974  xaddpnf1  10179  xaddmnf1  10181  xaddnemnf  10190  xaddnepnf  10191  xaddcom  10194  xnegdi  10201  xaddass  10202  xpncan  10204  xleadd1a  10206  xltadd1  10209  xlt2add  10213  modfzo0difsn  10757  frec2uzrdg  10771  seqf1oglem2  10882  expp1  10908  expnegap0  10909  expcllem  10912  mulexp  10940  expmul  10946  sqoddm1div8  11055  bcpasc  11128  hashfzo  11187  lsw0  11272  ccatval1  11285  ccatval2  11286  swrdval  11340  ccatopth  11408  reuccatpfxs1  11439  shftfn  11509  reim0b  11547  cjexp  11578  sumsnf  12095  binomlem  12169  prodsnf  12278  ef0lem  12346  dvdsnegb  12494  m1expe  12585  m1expo  12586  m1exp1  12587  flodddiv4  12622  gcdabs  12684  bezoutr1  12729  dvdslcm  12766  lcmeq0  12768  lcmcl  12769  lcmabs  12773  lcmgcdlem  12774  lcmdvds  12776  mulgcddvds  12791  qredeu  12794  divgcdcoprmex  12799  pcge0  13011  pcgcd1  13026  pcadd  13038  pcmpt2  13042  mulgfvalg  13838  mulgnn0subcl  13852  mulgnn0z  13866  f1ghm0to0  13989  srgmulgass  14133  srgpcomp  14134  ringinvnzdiv  14194  lmodvsmmulgdi  14471  znval  14784  mplvalcoe  14845  isxmet2d  15213  blfvalps  15250  blssioo  15418  efper  15672  relogbcxpbap  15830  logbgcd1irr  15832  lgsdir  15908  lgsne0  15911  lgsdirnn0  15920  lgsdinn0  15921  lgsquadlem2  15951  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  wlklenvm1  16336  wlklenvm1g  16337  wlk0prc  16367  clwwlkn2  16416  trirec0xor  16829