Theorem sylan9eqr 2286

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  sbcied2  3069  csbied2  3175  fun2ssres  5370  fcoi1  5517  fcoi2  5518  funssfv  5665  caovimo  6215  mpomptsx  6361  dmmpossx  6363  fmpox  6364  2ndconst  6386  mpoxopoveq  6405  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  rdgivallem  6546  nnmass  6654  nnm00  6697  ssenen  7036  fi0  7173  nnnninf2  7325  nnnninfeq2  7327  exmidfodomrlemim  7411  ltexnqq  7627  ltrnqg  7639  nqnq0a  7673  nqnq0m  7674  nq0m0r  7675  nq0a0  7676  addnqprllem  7746  addnqprulem  7747  map2psrprg  8024  rereceu  8108  addid0  8551  nnnn0addcl  9431  zindd  9597  qaddcl  9868  qmulcl  9870  qreccl  9875  xaddpnf1  10080  xaddmnf1  10082  xaddnemnf  10091  xaddnepnf  10092  xaddcom  10095  xnegdi  10102  xaddass  10103  xpncan  10105  xleadd1a  10107  xltadd1  10110  xlt2add  10114  modfzo0difsn  10656  frec2uzrdg  10670  seqf1oglem2  10781  expp1  10807  expnegap0  10808  expcllem  10811  mulexp  10839  expmul  10845  sqoddm1div8  10954  bcpasc  11027  hashfzo  11085  lsw0  11160  ccatval1  11173  ccatval2  11174  swrdval  11228  ccatopth  11296  reuccatpfxs1  11327  shftfn  11384  reim0b  11422  cjexp  11453  sumsnf  11969  binomlem  12043  prodsnf  12152  ef0lem  12220  dvdsnegb  12368  m1expe  12459  m1expo  12460  m1exp1  12461  flodddiv4  12496  gcdabs  12558  bezoutr1  12603  dvdslcm  12640  lcmeq0  12642  lcmcl  12643  lcmabs  12647  lcmgcdlem  12648  lcmdvds  12650  mulgcddvds  12665  qredeu  12668  divgcdcoprmex  12673  pcge0  12885  pcgcd1  12900  pcadd  12912  pcmpt2  12916  mulgfvalg  13707  mulgnn0subcl  13721  mulgnn0z  13735  f1ghm0to0  13858  srgmulgass  14001  srgpcomp  14002  ringinvnzdiv  14062  lmodvsmmulgdi  14336  znval  14649  mplvalcoe  14703  isxmet2d  15071  blfvalps  15108  blssioo  15276  efper  15530  relogbcxpbap  15688  logbgcd1irr  15690  lgsdir  15763  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  lgsquadlem2  15806  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  wlklenvm1  16191  wlklenvm1g  16192  wlk0prc  16222  clwwlkn2  16271  trirec0xor  16649