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  7467  nnnninfeq2  7469  exmidfodomrlemim  7553  ltexnqq  7775  ltrnqg  7787  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  nq0a0  7824  addnqprllem  7894  addnqprulem  7895  map2psrprg  8172  rereceu  8256  addid0  8699  nnnn0addcl  9593  zindd  9764  qaddcl  10035  qmulcl  10037  qreccl  10042  xaddpnf1  10248  xaddmnf1  10250  xaddnemnf  10259  xaddnepnf  10260  xaddcom  10263  xnegdi  10270  xaddass  10271  xpncan  10273  xleadd1a  10275  xltadd1  10278  xlt2add  10282  modfzo0difsn  10832  frec2uzrdg  10846  seqf1oglem2  10957  expp1  10983  expnegap0  10984  expcllem  10987  mulexp  11015  expmul  11021  sqoddm1div8  11131  bcpasc  11204  hashfzo  11263  hashf1lem1  11285  lsw0  11352  ccatval1  11365  ccatval2  11366  swrdval  11420  ccatopth  11488  reuccatpfxs1  11519  shftfn  11589  reim0b  11627  cjexp  11658  sumsnf  12176  binomlem  12250  prodsnf  12359  ef0lem  12427  dvdsnegb  12575  m1expe  12666  m1expo  12667  m1exp1  12668  flodddiv4  12703  gcdabs  12765  bezoutr1  12810  dvdslcm  12847  lcmeq0  12849  lcmcl  12850  lcmabs  12854  lcmgcdlem  12855  lcmdvds  12857  mulgcddvds  12872  qredeu  12875  divgcdcoprmex  12880  pcge0  13092  pcgcd1  13107  pcadd  13119  pcmpt2  13123  mulgfvalg  13924  mulgnn0subcl  13938  mulgnn0z  13952  f1ghm0to0  14075  srgmulgass  14293  srgpcomp  14294  ringinvnzdiv  14355  lmodvsmmulgdi  14660  znval  14971  assamulgscmlem2  15042  mplvalcoe  15081  isxmet2d  15449  blfvalps  15486  blssioo  15654  efper  15908  relogbcxpbap  16067  logbgcd1irr  16069  lgsdir  16154  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  lgsquadlem2  16197  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  wlklenvm1  16582  wlklenvm1g  16583  wlk0prc  16613  clwwlkn2  16662  trirec0xor  17094