Theorem sylan9eqr 2293

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  sbcied2  3089  csbied2  3195  fun2ssres  5421  fcoi1  5572  fcoi2  5573  funssfv  5721  caovimo  6283  mpomptsx  6433  dmmpossx  6435  fmpox  6436  2ndconst  6458  mpoxopoveq  6511  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  rdgivallem  6652  nnmass  6760  nnm00  6803  mapsnend  7099  ssenen  7152  fi0  7309  nnnninf2  7467  nnnninfeq2  7469  exmidfodomrlemim  7553  ltexnqq  7775  ltrnqg  7787  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  nq0a0  7824  addnqprllem  7894  addnqprulem  7895  map2psrprg  8172  rereceu  8256  addid0  8700  nnnn0addcl  9597  zindd  9768  qaddcl  10044  qmulcl  10046  qreccl  10051  xaddpnf1  10258  xaddmnf1  10260  xaddnemnf  10269  xaddnepnf  10270  xaddcom  10273  xnegdi  10280  xaddass  10281  xpncan  10283  xleadd1a  10285  xltadd1  10288  xlt2add  10292  modfzo0difsn  10845  frec2uzrdg  10859  seqf1oglem2  10970  expp1  10996  expnegap0  10997  expcllem  11000  mulexp  11028  expmul  11034  sqoddm1div8  11144  bcpasc  11218  hashfzo  11277  hashf1lem1  11299  lsw0  11366  ccatval1  11379  ccatval2  11380  swrdval  11434  ccatopth  11502  reuccatpfxs1  11533  shftfn  11603  reim0b  11641  cjexp  11672  sumsnf  12192  binomlem  12266  prodsnf  12375  ef0lem  12443  dvdsnegb  12591  m1expe  12682  m1expo  12683  m1exp1  12684  flodddiv4  12719  gcdabs  12781  bezoutr1  12826  dvdslcm  12863  lcmeq0  12865  lcmcl  12866  lcmabs  12870  lcmgcdlem  12871  lcmdvds  12873  mulgcddvds  12888  qredeu  12891  divgcdcoprmex  12896  pcge0  13112  pcgcd1  13127  pcadd  13139  pcmpt2  13143  mulgfvalg  13973  mulgnn0subcl  13987  mulgnn0z  14001  f1ghm0to0  14124  srgmulgass  14342  srgpcomp  14343  ringinvnzdiv  14404  lmodvsmmulgdi  14709  znval  15020  assamulgscmlem2  15091  mplvalcoe  15130  isxmet2d  15498  blfvalps  15535  blssioo  15703  efper  15958  relogbcxpbap  16120  logbgcd1irr  16122  zprmlogbaplem2  16135  bposlem2  16210  lgsdir  16252  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  lgsquadlem2  16295  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  wlklenvm1  16680  wlklenvm1g  16681  wlk0prc  16711  clwwlkn2  16760  trirec0xor  17192