Theorem sylan9eqr 2293

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

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  sbcied2  3089  csbied2  3195  fun2ssres  5416  fcoi1  5567  fcoi2  5568  funssfv  5716  caovimo  6273  mpomptsx  6423  dmmpossx  6425  fmpox  6426  2ndconst  6448  mpoxopoveq  6501  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  rdgivallem  6642  nnmass  6750  nnm00  6793  mapsnend  7089  ssenen  7142  fi0  7299  nnnninf2  7457  nnnninfeq2  7459  exmidfodomrlemim  7543  ltexnqq  7765  ltrnqg  7777  nqnq0a  7811  nqnq0m  7812  nq0m0r  7813  nq0a0  7814  addnqprllem  7884  addnqprulem  7885  map2psrprg  8162  rereceu  8246  addid0  8689  nnnn0addcl  9572  zindd  9743  qaddcl  10014  qmulcl  10016  qreccl  10021  xaddpnf1  10227  xaddmnf1  10229  xaddnemnf  10238  xaddnepnf  10239  xaddcom  10242  xnegdi  10249  xaddass  10250  xpncan  10252  xleadd1a  10254  xltadd1  10257  xlt2add  10261  modfzo0difsn  10810  frec2uzrdg  10824  seqf1oglem2  10935  expp1  10961  expnegap0  10962  expcllem  10965  mulexp  10993  expmul  10999  sqoddm1div8  11109  bcpasc  11182  hashfzo  11241  hashf1lem1  11263  lsw0  11330  ccatval1  11343  ccatval2  11344  swrdval  11398  ccatopth  11466  reuccatpfxs1  11497  shftfn  11567  reim0b  11605  cjexp  11636  sumsnf  12154  binomlem  12228  prodsnf  12337  ef0lem  12405  dvdsnegb  12553  m1expe  12644  m1expo  12645  m1exp1  12646  flodddiv4  12681  gcdabs  12743  bezoutr1  12788  dvdslcm  12825  lcmeq0  12827  lcmcl  12828  lcmabs  12832  lcmgcdlem  12833  lcmdvds  12835  mulgcddvds  12850  qredeu  12853  divgcdcoprmex  12858  pcge0  13070  pcgcd1  13085  pcadd  13097  pcmpt2  13101  mulgfvalg  13901  mulgnn0subcl  13915  mulgnn0z  13929  f1ghm0to0  14052  srgmulgass  14267  srgpcomp  14268  ringinvnzdiv  14328  lmodvsmmulgdi  14632  znval  14943  mplvalcoe  15004  isxmet2d  15372  blfvalps  15409  blssioo  15577  efper  15831  relogbcxpbap  15990  logbgcd1irr  15992  lgsdir  16068  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  lgsquadlem2  16111  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  wlklenvm1  16496  wlklenvm1g  16497  wlk0prc  16527  clwwlkn2  16576  trirec0xor  16999