Theorem sylan9eqr 2244

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  sbcied2  3015  csbied2  3119  fun2ssres  5274  fcoi1  5411  fcoi2  5412  funssfv  5556  caovimo  6085  mpomptsx  6216  dmmpossx  6218  fmpox  6219  2ndconst  6241  mpoxopoveq  6259  tfrlemisucaccv  6344  tfr1onlemsucaccv  6360  tfrcllemsucaccv  6373  rdgivallem  6400  nnmass  6506  nnm00  6549  ssenen  6869  fi0  6992  nnnninf2  7143  nnnninfeq2  7145  exmidfodomrlemim  7218  ltexnqq  7425  ltrnqg  7437  nqnq0a  7471  nqnq0m  7472  nq0m0r  7473  nq0a0  7474  addnqprllem  7544  addnqprulem  7545  map2psrprg  7822  rereceu  7906  addid0  8348  nnnn0addcl  9224  zindd  9389  qaddcl  9653  qmulcl  9655  qreccl  9660  xaddpnf1  9864  xaddmnf1  9866  xaddnemnf  9875  xaddnepnf  9876  xaddcom  9879  xnegdi  9886  xaddass  9887  xpncan  9889  xleadd1a  9891  xltadd1  9894  xlt2add  9898  modfzo0difsn  10413  frec2uzrdg  10427  expp1  10545  expnegap0  10546  expcllem  10549  mulexp  10577  expmul  10583  sqoddm1div8  10692  bcpasc  10764  hashfzo  10820  shftfn  10851  reim0b  10889  cjexp  10920  sumsnf  11435  binomlem  11509  prodsnf  11618  ef0lem  11686  dvdsnegb  11833  m1expe  11922  m1expo  11923  m1exp1  11924  flodddiv4  11957  gcdabs  12007  bezoutr1  12052  dvdslcm  12087  lcmeq0  12089  lcmcl  12090  lcmabs  12094  lcmgcdlem  12095  lcmdvds  12097  mulgcddvds  12112  qredeu  12115  divgcdcoprmex  12120  pcge0  12330  pcgcd1  12345  pcadd  12357  pcmpt2  12360  mulgfvalg  13029  mulgnn0subcl  13041  mulgnn0z  13055  f1ghm0to0  13172  srgmulgass  13304  srgpcomp  13305  ringinvnzdiv  13363  lmodvsmmulgdi  13600  znval  13893  isxmet2d  14245  blfvalps  14282  blssioo  14442  efper  14625  relogbcxpbap  14780  logbgcd1irr  14782  lgsdir  14833  lgsne0  14836  lgsdirnn0  14845  lgsdinn0  14846  trirec0xor  15191