Theorem sylan9eqr 2225

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  sbcied2  2992  csbied2  3096  fun2ssres  5239  fcoi1  5376  fcoi2  5377  funssfv  5520  caovimo  6043  mpomptsx  6173  dmmpossx  6175  fmpox  6176  2ndconst  6198  mpoxopoveq  6216  tfrlemisucaccv  6301  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  rdgivallem  6357  nnmass  6463  nnm00  6505  ssenen  6825  fi0  6948  nnnninf2  7099  nnnninfeq2  7101  exmidfodomrlemim  7165  ltexnqq  7357  ltrnqg  7369  nqnq0a  7403  nqnq0m  7404  nq0m0r  7405  nq0a0  7406  addnqprllem  7476  addnqprulem  7477  map2psrprg  7754  rereceu  7838  addid0  8279  nnnn0addcl  9152  zindd  9317  qaddcl  9581  qmulcl  9583  qreccl  9588  xaddpnf1  9790  xaddmnf1  9792  xaddnemnf  9801  xaddnepnf  9802  xaddcom  9805  xnegdi  9812  xaddass  9813  xpncan  9815  xleadd1a  9817  xltadd1  9820  xlt2add  9824  modfzo0difsn  10338  frec2uzrdg  10352  expp1  10470  expnegap0  10471  expcllem  10474  mulexp  10502  expmul  10508  sqoddm1div8  10616  bcpasc  10687  hashfzo  10744  shftfn  10775  reim0b  10813  cjexp  10844  sumsnf  11359  binomlem  11433  prodsnf  11542  ef0lem  11610  dvdsnegb  11757  m1expe  11845  m1expo  11846  m1exp1  11847  flodddiv4  11880  gcdabs  11930  bezoutr1  11975  dvdslcm  12010  lcmeq0  12012  lcmcl  12013  lcmabs  12017  lcmgcdlem  12018  lcmdvds  12020  mulgcddvds  12035  qredeu  12038  divgcdcoprmex  12043  pcge0  12253  pcgcd1  12268  pcadd  12280  pcmpt2  12283  isxmet2d  13101  blfvalps  13138  blssioo  13298  efper  13481  relogbcxpbap  13636  logbgcd1irr  13638  lgsdir  13689  lgsne0  13692  lgsdirnn0  13701  lgsdinn0  13702  trirec0xor  14037