Theorem sylan9eqr 2260

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  sbcied2  3036  csbied2  3141  fun2ssres  5314  fcoi1  5456  fcoi2  5457  funssfv  5602  caovimo  6140  mpomptsx  6283  dmmpossx  6285  fmpox  6286  2ndconst  6308  mpoxopoveq  6326  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  rdgivallem  6467  nnmass  6573  nnm00  6616  ssenen  6948  fi0  7077  nnnninf2  7229  nnnninfeq2  7231  exmidfodomrlemim  7309  ltexnqq  7521  ltrnqg  7533  nqnq0a  7567  nqnq0m  7568  nq0m0r  7569  nq0a0  7570  addnqprllem  7640  addnqprulem  7641  map2psrprg  7918  rereceu  8002  addid0  8445  nnnn0addcl  9325  zindd  9491  qaddcl  9756  qmulcl  9758  qreccl  9763  xaddpnf1  9968  xaddmnf1  9970  xaddnemnf  9979  xaddnepnf  9980  xaddcom  9983  xnegdi  9990  xaddass  9991  xpncan  9993  xleadd1a  9995  xltadd1  9998  xlt2add  10002  modfzo0difsn  10540  frec2uzrdg  10554  seqf1oglem2  10665  expp1  10691  expnegap0  10692  expcllem  10695  mulexp  10723  expmul  10729  sqoddm1div8  10838  bcpasc  10911  hashfzo  10967  lsw0  11041  ccatval1  11053  ccatval2  11054  swrdval  11101  shftfn  11135  reim0b  11173  cjexp  11204  sumsnf  11720  binomlem  11794  prodsnf  11903  ef0lem  11971  dvdsnegb  12119  m1expe  12210  m1expo  12211  m1exp1  12212  flodddiv4  12247  gcdabs  12309  bezoutr1  12354  dvdslcm  12391  lcmeq0  12393  lcmcl  12394  lcmabs  12398  lcmgcdlem  12399  lcmdvds  12401  mulgcddvds  12416  qredeu  12419  divgcdcoprmex  12424  pcge0  12636  pcgcd1  12651  pcadd  12663  pcmpt2  12667  mulgfvalg  13457  mulgnn0subcl  13471  mulgnn0z  13485  f1ghm0to0  13608  srgmulgass  13751  srgpcomp  13752  ringinvnzdiv  13812  lmodvsmmulgdi  14085  znval  14398  mplvalcoe  14452  isxmet2d  14820  blfvalps  14857  blssioo  15025  efper  15279  relogbcxpbap  15437  logbgcd1irr  15439  lgsdir  15512  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  lgsquadlem2  15555  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  trirec0xor  15984