Theorem sylan9eqr 2262

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 2260	. 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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  sbcied2  3043  csbied2  3149  fun2ssres  5333  fcoi1  5478  fcoi2  5479  funssfv  5625  caovimo  6163  mpomptsx  6306  dmmpossx  6308  fmpox  6309  2ndconst  6331  mpoxopoveq  6349  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  rdgivallem  6490  nnmass  6596  nnm00  6639  ssenen  6973  fi0  7103  nnnninf2  7255  nnnninfeq2  7257  exmidfodomrlemim  7340  ltexnqq  7556  ltrnqg  7568  nqnq0a  7602  nqnq0m  7603  nq0m0r  7604  nq0a0  7605  addnqprllem  7675  addnqprulem  7676  map2psrprg  7953  rereceu  8037  addid0  8480  nnnn0addcl  9360  zindd  9526  qaddcl  9791  qmulcl  9793  qreccl  9798  xaddpnf1  10003  xaddmnf1  10005  xaddnemnf  10014  xaddnepnf  10015  xaddcom  10018  xnegdi  10025  xaddass  10026  xpncan  10028  xleadd1a  10030  xltadd1  10033  xlt2add  10037  modfzo0difsn  10577  frec2uzrdg  10591  seqf1oglem2  10702  expp1  10728  expnegap0  10729  expcllem  10732  mulexp  10760  expmul  10766  sqoddm1div8  10875  bcpasc  10948  hashfzo  11004  lsw0  11078  ccatval1  11091  ccatval2  11092  swrdval  11139  ccatopth  11207  reuccatpfxs1  11238  shftfn  11250  reim0b  11288  cjexp  11319  sumsnf  11835  binomlem  11909  prodsnf  12018  ef0lem  12086  dvdsnegb  12234  m1expe  12325  m1expo  12326  m1exp1  12327  flodddiv4  12362  gcdabs  12424  bezoutr1  12469  dvdslcm  12506  lcmeq0  12508  lcmcl  12509  lcmabs  12513  lcmgcdlem  12514  lcmdvds  12516  mulgcddvds  12531  qredeu  12534  divgcdcoprmex  12539  pcge0  12751  pcgcd1  12766  pcadd  12778  pcmpt2  12782  mulgfvalg  13572  mulgnn0subcl  13586  mulgnn0z  13600  f1ghm0to0  13723  srgmulgass  13866  srgpcomp  13867  ringinvnzdiv  13927  lmodvsmmulgdi  14200  znval  14513  mplvalcoe  14567  isxmet2d  14935  blfvalps  14972  blssioo  15140  efper  15394  relogbcxpbap  15552  logbgcd1irr  15554  lgsdir  15627  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  lgsquadlem2  15670  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692  trirec0xor  16186