Theorem sylan9eqr 2260

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  sbcied2  3036  csbied2  3141  fun2ssres  5315  fcoi1  5458  fcoi2  5459  funssfv  5604  caovimo  6142  mpomptsx  6285  dmmpossx  6287  fmpox  6288  2ndconst  6310  mpoxopoveq  6328  tfrlemisucaccv  6413  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  rdgivallem  6469  nnmass  6575  nnm00  6618  ssenen  6950  fi0  7079  nnnninf2  7231  nnnninfeq2  7233  exmidfodomrlemim  7311  ltexnqq  7523  ltrnqg  7535  nqnq0a  7569  nqnq0m  7570  nq0m0r  7571  nq0a0  7572  addnqprllem  7642  addnqprulem  7643  map2psrprg  7920  rereceu  8004  addid0  8447  nnnn0addcl  9327  zindd  9493  qaddcl  9758  qmulcl  9760  qreccl  9765  xaddpnf1  9970  xaddmnf1  9972  xaddnemnf  9981  xaddnepnf  9982  xaddcom  9985  xnegdi  9992  xaddass  9993  xpncan  9995  xleadd1a  9997  xltadd1  10000  xlt2add  10004  modfzo0difsn  10542  frec2uzrdg  10556  seqf1oglem2  10667  expp1  10693  expnegap0  10694  expcllem  10697  mulexp  10725  expmul  10731  sqoddm1div8  10840  bcpasc  10913  hashfzo  10969  lsw0  11043  ccatval1  11056  ccatval2  11057  swrdval  11104  shftfn  11168  reim0b  11206  cjexp  11237  sumsnf  11753  binomlem  11827  prodsnf  11936  ef0lem  12004  dvdsnegb  12152  m1expe  12243  m1expo  12244  m1exp1  12245  flodddiv4  12280  gcdabs  12342  bezoutr1  12387  dvdslcm  12424  lcmeq0  12426  lcmcl  12427  lcmabs  12431  lcmgcdlem  12432  lcmdvds  12434  mulgcddvds  12449  qredeu  12452  divgcdcoprmex  12457  pcge0  12669  pcgcd1  12684  pcadd  12696  pcmpt2  12700  mulgfvalg  13490  mulgnn0subcl  13504  mulgnn0z  13518  f1ghm0to0  13641  srgmulgass  13784  srgpcomp  13785  ringinvnzdiv  13845  lmodvsmmulgdi  14118  znval  14431  mplvalcoe  14485  isxmet2d  14853  blfvalps  14890  blssioo  15058  efper  15312  relogbcxpbap  15470  logbgcd1irr  15472  lgsdir  15545  lgsne0  15548  lgsdirnn0  15557  lgsdinn0  15558  lgsquadlem2  15588  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgslem3a1  15607  2lgslem3b1  15608  2lgslem3c1  15609  2lgslem3d1  15610  trirec0xor  16021