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  5424  fcoi1  5575  fcoi2  5576  funssfv  5724  caovimo  6286  mpomptsx  6437  dmmpossx  6439  fmpox  6440  2ndconst  6462  mpoxopoveq  6515  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  rdgivallem  6656  nnmass  6764  nnm00  6807  mapsnend  7103  ssenen  7156  fi0  7314  nnnninf2  7473  nnnninfeq2  7475  exmidfodomrlemim  7559  ltexnqq  7781  ltrnqg  7793  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  nq0a0  7830  addnqprllem  7900  addnqprulem  7901  map2psrprg  8178  rereceu  8262  addid0  8706  nnnn0addcl  9604  zindd  9775  qaddcl  10051  qmulcl  10053  qreccl  10058  xaddpnf1  10265  xaddmnf1  10267  xaddnemnf  10276  xaddnepnf  10277  xaddcom  10280  xnegdi  10287  xaddass  10288  xpncan  10290  xleadd1a  10292  xltadd1  10295  xlt2add  10299  modfzo0difsn  10853  frec2uzrdg  10867  seqf1oglem2  10978  expp1  11004  expnegap0  11005  expcllem  11008  mulexp  11036  expmul  11042  sqoddm1div8  11152  bcpasc  11226  hashfzo  11285  hashf1lem1  11307  lsw0  11374  ccatval1  11387  ccatval2  11388  swrdval  11442  ccatopth  11510  reuccatpfxs1  11541  shftfn  11611  reim0b  11649  cjexp  11680  sumsnf  12201  binomlem  12275  prodsnf  12384  ef0lem  12452  dvdsnegb  12600  m1expe  12691  m1expo  12692  m1exp1  12693  flodddiv4  12728  gcdabs  12790  bezoutr1  12835  dvdslcm  12872  lcmeq0  12874  lcmcl  12875  lcmabs  12879  lcmgcdlem  12880  lcmdvds  12882  mulgcddvds  12897  qredeu  12900  divgcdcoprmex  12905  pcge0  13121  pcgcd1  13136  pcadd  13148  pcmpt2  13152  mulgfvalg  13983  mulgnn0subcl  13997  mulgnn0z  14011  f1ghm0to0  14134  gsumresfi  14263  srgmulgass  14400  srgpcomp  14401  ringinvnzdiv  14462  lmodvsmmulgdi  14769  znval  15080  assamulgscmlem2  15151  mplvalcoe  15206  isxmet2d  15574  blfvalps  15611  blssioo  15779  efper  16034  relogbcxpbap  16201  logbgcd1irr  16203  zprmlogbaplem2  16216  chtqub  16296  bposlem2  16312  lgsdir  16359  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  lgsquadlem2  16402  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  wlklenvm1  16787  wlklenvm1g  16788  wlk0prc  16818  clwwlkn2  16867  trirec0xor  17301