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  5508  fcoi2  5509  funssfv  5655  caovimo  6205  mpomptsx  6349  dmmpossx  6351  fmpox  6352  2ndconst  6374  mpoxopoveq  6392  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  rdgivallem  6533  nnmass  6641  nnm00  6684  ssenen  7020  fi0  7153  nnnninf2  7305  nnnninfeq2  7307  exmidfodomrlemim  7390  ltexnqq  7606  ltrnqg  7618  nqnq0a  7652  nqnq0m  7653  nq0m0r  7654  nq0a0  7655  addnqprllem  7725  addnqprulem  7726  map2psrprg  8003  rereceu  8087  addid0  8530  nnnn0addcl  9410  zindd  9576  qaddcl  9842  qmulcl  9844  qreccl  9849  xaddpnf1  10054  xaddmnf1  10056  xaddnemnf  10065  xaddnepnf  10066  xaddcom  10069  xnegdi  10076  xaddass  10077  xpncan  10079  xleadd1a  10081  xltadd1  10084  xlt2add  10088  modfzo0difsn  10629  frec2uzrdg  10643  seqf1oglem2  10754  expp1  10780  expnegap0  10781  expcllem  10784  mulexp  10812  expmul  10818  sqoddm1div8  10927  bcpasc  11000  hashfzo  11057  lsw0  11132  ccatval1  11145  ccatval2  11146  swrdval  11196  ccatopth  11264  reuccatpfxs1  11295  shftfn  11351  reim0b  11389  cjexp  11420  sumsnf  11936  binomlem  12010  prodsnf  12119  ef0lem  12187  dvdsnegb  12335  m1expe  12426  m1expo  12427  m1exp1  12428  flodddiv4  12463  gcdabs  12525  bezoutr1  12570  dvdslcm  12607  lcmeq0  12609  lcmcl  12610  lcmabs  12614  lcmgcdlem  12615  lcmdvds  12617  mulgcddvds  12632  qredeu  12635  divgcdcoprmex  12640  pcge0  12852  pcgcd1  12867  pcadd  12879  pcmpt2  12883  mulgfvalg  13674  mulgnn0subcl  13688  mulgnn0z  13702  f1ghm0to0  13825  srgmulgass  13968  srgpcomp  13969  ringinvnzdiv  14029  lmodvsmmulgdi  14303  znval  14616  mplvalcoe  14670  isxmet2d  15038  blfvalps  15075  blssioo  15243  efper  15497  relogbcxpbap  15655  logbgcd1irr  15657  lgsdir  15730  lgsne0  15733  lgsdirnn0  15742  lgsdinn0  15743  lgsquadlem2  15773  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  wlklenvm1  16087  wlklenvm1g  16088  wlk0prc  16118  clwwlkn2  16163  trirec0xor  16501