Theorem sylan9eqr 2293

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  sbcied2  3089  csbied2  3195  fun2ssres  5421  fcoi1  5572  fcoi2  5573  funssfv  5721  caovimo  6283  mpomptsx  6433  dmmpossx  6435  fmpox  6436  2ndconst  6458  mpoxopoveq  6511  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  rdgivallem  6652  nnmass  6760  nnm00  6803  mapsnend  7099  ssenen  7152  fi0  7309  nnnninf2  7468  nnnninfeq2  7470  exmidfodomrlemim  7554  ltexnqq  7776  ltrnqg  7788  nqnq0a  7822  nqnq0m  7823  nq0m0r  7824  nq0a0  7825  addnqprllem  7895  addnqprulem  7896  map2psrprg  8173  rereceu  8257  addid0  8701  nnnn0addcl  9598  zindd  9769  qaddcl  10045  qmulcl  10047  qreccl  10052  xaddpnf1  10259  xaddmnf1  10261  xaddnemnf  10270  xaddnepnf  10271  xaddcom  10274  xnegdi  10281  xaddass  10282  xpncan  10284  xleadd1a  10286  xltadd1  10289  xlt2add  10293  modfzo0difsn  10847  frec2uzrdg  10861  seqf1oglem2  10972  expp1  10998  expnegap0  10999  expcllem  11002  mulexp  11030  expmul  11036  sqoddm1div8  11146  bcpasc  11220  hashfzo  11279  hashf1lem1  11301  lsw0  11368  ccatval1  11381  ccatval2  11382  swrdval  11436  ccatopth  11504  reuccatpfxs1  11535  shftfn  11605  reim0b  11643  cjexp  11674  sumsnf  12195  binomlem  12269  prodsnf  12378  ef0lem  12446  dvdsnegb  12594  m1expe  12685  m1expo  12686  m1exp1  12687  flodddiv4  12722  gcdabs  12784  bezoutr1  12829  dvdslcm  12866  lcmeq0  12868  lcmcl  12869  lcmabs  12873  lcmgcdlem  12874  lcmdvds  12876  mulgcddvds  12891  qredeu  12894  divgcdcoprmex  12899  pcge0  13115  pcgcd1  13130  pcadd  13142  pcmpt2  13146  mulgfvalg  13977  mulgnn0subcl  13991  mulgnn0z  14005  f1ghm0to0  14128  srgmulgass  14377  srgpcomp  14378  ringinvnzdiv  14439  lmodvsmmulgdi  14744  znval  15055  assamulgscmlem2  15126  mplvalcoe  15172  isxmet2d  15540  blfvalps  15577  blssioo  15745  efper  16000  relogbcxpbap  16162  logbgcd1irr  16164  zprmlogbaplem2  16177  chtqub  16257  bposlem2  16273  lgsdir  16320  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  lgsquadlem2  16363  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  wlklenvm1  16748  wlklenvm1g  16749  wlk0prc  16779  clwwlkn2  16828  trirec0xor  17261