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  3066  csbied2  3172  fun2ssres  5361  fcoi1  5506  fcoi2  5507  funssfv  5653  caovimo  6199  mpomptsx  6343  dmmpossx  6345  fmpox  6346  2ndconst  6368  mpoxopoveq  6386  tfrlemisucaccv  6471  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  rdgivallem  6527  nnmass  6633  nnm00  6676  ssenen  7012  fi0  7142  nnnninf2  7294  nnnninfeq2  7296  exmidfodomrlemim  7379  ltexnqq  7595  ltrnqg  7607  nqnq0a  7641  nqnq0m  7642  nq0m0r  7643  nq0a0  7644  addnqprllem  7714  addnqprulem  7715  map2psrprg  7992  rereceu  8076  addid0  8519  nnnn0addcl  9399  zindd  9565  qaddcl  9830  qmulcl  9832  qreccl  9837  xaddpnf1  10042  xaddmnf1  10044  xaddnemnf  10053  xaddnepnf  10054  xaddcom  10057  xnegdi  10064  xaddass  10065  xpncan  10067  xleadd1a  10069  xltadd1  10072  xlt2add  10076  modfzo0difsn  10617  frec2uzrdg  10631  seqf1oglem2  10742  expp1  10768  expnegap0  10769  expcllem  10772  mulexp  10800  expmul  10806  sqoddm1div8  10915  bcpasc  10988  hashfzo  11044  lsw0  11119  ccatval1  11132  ccatval2  11133  swrdval  11180  ccatopth  11248  reuccatpfxs1  11279  shftfn  11335  reim0b  11373  cjexp  11404  sumsnf  11920  binomlem  11994  prodsnf  12103  ef0lem  12171  dvdsnegb  12319  m1expe  12410  m1expo  12411  m1exp1  12412  flodddiv4  12447  gcdabs  12509  bezoutr1  12554  dvdslcm  12591  lcmeq0  12593  lcmcl  12594  lcmabs  12598  lcmgcdlem  12599  lcmdvds  12601  mulgcddvds  12616  qredeu  12619  divgcdcoprmex  12624  pcge0  12836  pcgcd1  12851  pcadd  12863  pcmpt2  12867  mulgfvalg  13658  mulgnn0subcl  13672  mulgnn0z  13686  f1ghm0to0  13809  srgmulgass  13952  srgpcomp  13953  ringinvnzdiv  14013  lmodvsmmulgdi  14287  znval  14600  mplvalcoe  14654  isxmet2d  15022  blfvalps  15059  blssioo  15227  efper  15481  relogbcxpbap  15639  logbgcd1irr  15641  lgsdir  15714  lgsne0  15717  lgsdirnn0  15726  lgsdinn0  15727  lgsquadlem2  15757  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  wlklenvm1  16052  wlklenvm1g  16053  wlk0prc  16083  trirec0xor  16413