Theorem sylan9eqr 2232

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  sbcied2  3002  csbied2  3106  fun2ssres  5261  fcoi1  5398  fcoi2  5399  funssfv  5543  caovimo  6070  mpomptsx  6200  dmmpossx  6202  fmpox  6203  2ndconst  6225  mpoxopoveq  6243  tfrlemisucaccv  6328  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  rdgivallem  6384  nnmass  6490  nnm00  6533  ssenen  6853  fi0  6976  nnnninf2  7127  nnnninfeq2  7129  exmidfodomrlemim  7202  ltexnqq  7409  ltrnqg  7421  nqnq0a  7455  nqnq0m  7456  nq0m0r  7457  nq0a0  7458  addnqprllem  7528  addnqprulem  7529  map2psrprg  7806  rereceu  7890  addid0  8332  nnnn0addcl  9208  zindd  9373  qaddcl  9637  qmulcl  9639  qreccl  9644  xaddpnf1  9848  xaddmnf1  9850  xaddnemnf  9859  xaddnepnf  9860  xaddcom  9863  xnegdi  9870  xaddass  9871  xpncan  9873  xleadd1a  9875  xltadd1  9878  xlt2add  9882  modfzo0difsn  10397  frec2uzrdg  10411  expp1  10529  expnegap0  10530  expcllem  10533  mulexp  10561  expmul  10567  sqoddm1div8  10676  bcpasc  10748  hashfzo  10804  shftfn  10835  reim0b  10873  cjexp  10904  sumsnf  11419  binomlem  11493  prodsnf  11602  ef0lem  11670  dvdsnegb  11817  m1expe  11906  m1expo  11907  m1exp1  11908  flodddiv4  11941  gcdabs  11991  bezoutr1  12036  dvdslcm  12071  lcmeq0  12073  lcmcl  12074  lcmabs  12078  lcmgcdlem  12079  lcmdvds  12081  mulgcddvds  12096  qredeu  12099  divgcdcoprmex  12104  pcge0  12314  pcgcd1  12329  pcadd  12341  pcmpt2  12344  mulgfvalg  12990  mulgnn0subcl  13001  mulgnn0z  13015  srgmulgass  13177  srgpcomp  13178  ringinvnzdiv  13232  lmodvsmmulgdi  13418  isxmet2d  13887  blfvalps  13924  blssioo  14084  efper  14267  relogbcxpbap  14422  logbgcd1irr  14424  lgsdir  14475  lgsne0  14478  lgsdirnn0  14487  lgsdinn0  14488  trirec0xor  14832