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 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 2213

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

This theorem is referenced by:  sbcied2  3070  csbied2  3176  fun2ssres  5377  fcoi1  5525  fcoi2  5526  funssfv  5674  caovimo  6226  mpomptsx  6371  dmmpossx  6373  fmpox  6374  2ndconst  6396  mpoxopoveq  6449  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  rdgivallem  6590  nnmass  6698  nnm00  6741  ssenen  7080  fi0  7234  nnnninf2  7386  nnnninfeq2  7388  exmidfodomrlemim  7472  ltexnqq  7688  ltrnqg  7700  nqnq0a  7734  nqnq0m  7735  nq0m0r  7736  nq0a0  7737  addnqprllem  7807  addnqprulem  7808  map2psrprg  8085  rereceu  8169  addid0  8611  nnnn0addcl  9491  zindd  9659  qaddcl  9930  qmulcl  9932  qreccl  9937  xaddpnf1  10142  xaddmnf1  10144  xaddnemnf  10153  xaddnepnf  10154  xaddcom  10157  xnegdi  10164  xaddass  10165  xpncan  10167  xleadd1a  10169  xltadd1  10172  xlt2add  10176  modfzo0difsn  10720  frec2uzrdg  10734  seqf1oglem2  10845  expp1  10871  expnegap0  10872  expcllem  10875  mulexp  10903  expmul  10909  sqoddm1div8  11018  bcpasc  11091  hashfzo  11149  lsw0  11227  ccatval1  11240  ccatval2  11241  swrdval  11295  ccatopth  11363  reuccatpfxs1  11394  shftfn  11464  reim0b  11502  cjexp  11533  sumsnf  12050  binomlem  12124  prodsnf  12233  ef0lem  12301  dvdsnegb  12449  m1expe  12540  m1expo  12541  m1exp1  12542  flodddiv4  12577  gcdabs  12639  bezoutr1  12684  dvdslcm  12721  lcmeq0  12723  lcmcl  12724  lcmabs  12728  lcmgcdlem  12729  lcmdvds  12731  mulgcddvds  12746  qredeu  12749  divgcdcoprmex  12754  pcge0  12966  pcgcd1  12981  pcadd  12993  pcmpt2  12997  mulgfvalg  13788  mulgnn0subcl  13802  mulgnn0z  13816  f1ghm0to0  13939  srgmulgass  14083  srgpcomp  14084  ringinvnzdiv  14144  lmodvsmmulgdi  14419  znval  14732  mplvalcoe  14791  isxmet2d  15159  blfvalps  15196  blssioo  15364  efper  15618  relogbcxpbap  15776  logbgcd1irr  15778  lgsdir  15854  lgsne0  15857  lgsdirnn0  15866  lgsdinn0  15867  lgsquadlem2  15897  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgslem3a1  15916  2lgslem3b1  15917  2lgslem3c1  15918  2lgslem3d1  15919  wlklenvm1  16282  wlklenvm1g  16283  wlk0prc  16313  clwwlkn2  16362  trirec0xor  16777