Theorem sylan9eqr 2289

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 2287	. 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 2216

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

This theorem is referenced by:  sbcied2  3083  csbied2  3189  fun2ssres  5401  fcoi1  5552  fcoi2  5553  funssfv  5701  caovimo  6256  mpomptsx  6406  dmmpossx  6408  fmpox  6409  2ndconst  6431  mpoxopoveq  6484  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  rdgivallem  6625  nnmass  6733  nnm00  6776  mapsnend  7065  ssenen  7118  fi0  7275  nnnninf2  7431  nnnninfeq2  7433  exmidfodomrlemim  7517  ltexnqq  7739  ltrnqg  7751  nqnq0a  7785  nqnq0m  7786  nq0m0r  7787  nq0a0  7788  addnqprllem  7858  addnqprulem  7859  map2psrprg  8136  rereceu  8220  addid0  8662  nnnn0addcl  9543  zindd  9714  qaddcl  9985  qmulcl  9987  qreccl  9992  xaddpnf1  10198  xaddmnf1  10200  xaddnemnf  10209  xaddnepnf  10210  xaddcom  10213  xnegdi  10220  xaddass  10221  xpncan  10223  xleadd1a  10225  xltadd1  10228  xlt2add  10232  modfzo0difsn  10781  frec2uzrdg  10795  seqf1oglem2  10906  expp1  10932  expnegap0  10933  expcllem  10936  mulexp  10964  expmul  10970  sqoddm1div8  11080  bcpasc  11153  hashfzo  11212  lsw0  11297  ccatval1  11310  ccatval2  11311  swrdval  11365  ccatopth  11433  reuccatpfxs1  11464  shftfn  11534  reim0b  11572  cjexp  11603  sumsnf  12120  binomlem  12194  prodsnf  12303  ef0lem  12371  dvdsnegb  12519  m1expe  12610  m1expo  12611  m1exp1  12612  flodddiv4  12647  gcdabs  12709  bezoutr1  12754  dvdslcm  12791  lcmeq0  12793  lcmcl  12794  lcmabs  12798  lcmgcdlem  12799  lcmdvds  12801  mulgcddvds  12816  qredeu  12819  divgcdcoprmex  12824  pcge0  13036  pcgcd1  13051  pcadd  13063  pcmpt2  13067  mulgfvalg  13874  mulgnn0subcl  13888  mulgnn0z  13902  f1ghm0to0  14025  srgmulgass  14232  srgpcomp  14233  ringinvnzdiv  14293  lmodvsmmulgdi  14597  znval  14910  mplvalcoe  14971  isxmet2d  15339  blfvalps  15376  blssioo  15544  efper  15798  relogbcxpbap  15956  logbgcd1irr  15958  lgsdir  16034  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  lgsquadlem2  16077  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  wlklenvm1  16462  wlklenvm1g  16463  wlk0prc  16493  clwwlkn2  16542  trirec0xor  16955