Theorem sylan9eqr 2284

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  sbcied2  3067  csbied2  3173  fun2ssres  5367  fcoi1  5514  fcoi2  5515  funssfv  5661  caovimo  6211  mpomptsx  6357  dmmpossx  6359  fmpox  6360  2ndconst  6382  mpoxopoveq  6401  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  rdgivallem  6542  nnmass  6650  nnm00  6693  ssenen  7032  fi0  7165  nnnninf2  7317  nnnninfeq2  7319  exmidfodomrlemim  7402  ltexnqq  7618  ltrnqg  7630  nqnq0a  7664  nqnq0m  7665  nq0m0r  7666  nq0a0  7667  addnqprllem  7737  addnqprulem  7738  map2psrprg  8015  rereceu  8099  addid0  8542  nnnn0addcl  9422  zindd  9588  qaddcl  9859  qmulcl  9861  qreccl  9866  xaddpnf1  10071  xaddmnf1  10073  xaddnemnf  10082  xaddnepnf  10083  xaddcom  10086  xnegdi  10093  xaddass  10094  xpncan  10096  xleadd1a  10098  xltadd1  10101  xlt2add  10105  modfzo0difsn  10647  frec2uzrdg  10661  seqf1oglem2  10772  expp1  10798  expnegap0  10799  expcllem  10802  mulexp  10830  expmul  10836  sqoddm1div8  10945  bcpasc  11018  hashfzo  11076  lsw0  11151  ccatval1  11164  ccatval2  11165  swrdval  11219  ccatopth  11287  reuccatpfxs1  11318  shftfn  11375  reim0b  11413  cjexp  11444  sumsnf  11960  binomlem  12034  prodsnf  12143  ef0lem  12211  dvdsnegb  12359  m1expe  12450  m1expo  12451  m1exp1  12452  flodddiv4  12487  gcdabs  12549  bezoutr1  12594  dvdslcm  12631  lcmeq0  12633  lcmcl  12634  lcmabs  12638  lcmgcdlem  12639  lcmdvds  12641  mulgcddvds  12656  qredeu  12659  divgcdcoprmex  12664  pcge0  12876  pcgcd1  12891  pcadd  12903  pcmpt2  12907  mulgfvalg  13698  mulgnn0subcl  13712  mulgnn0z  13726  f1ghm0to0  13849  srgmulgass  13992  srgpcomp  13993  ringinvnzdiv  14053  lmodvsmmulgdi  14327  znval  14640  mplvalcoe  14694  isxmet2d  15062  blfvalps  15099  blssioo  15267  efper  15521  relogbcxpbap  15679  logbgcd1irr  15681  lgsdir  15754  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  lgsquadlem2  15797  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  wlklenvm1  16138  wlklenvm1g  16139  wlk0prc  16169  clwwlkn2  16216  trirec0xor  16585