Theorem sylan9eqr 2678

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

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  sbcied2  3473  csbied2  3561  fun2ssres  5931  fcoi1  6078  fcoi2  6079  funssfv  6209  fvtp1  6460  nvof1o  6536  onuninsuci  7040  ot1stg  7182  ot2ndg  7183  el2xptp0  7212  mpt2mptsx  7233  dmmpt2ssx  7235  fmpt2x  7236  2ndconst  7266  mpt2xopoveq  7345  wfrlem10  7424  rdgeq12  7509  rdgsucmptnf  7525  frsucmptn  7534  oev2  7603  oesuclem  7605  oawordeulem  7634  om00  7655  omass  7660  oeoa  7677  oeoe  7679  nnmass  7704  oaabs2  7725  omabs  7727  omxpenlem  8061  sbthlem4  8073  sbthlem6  8075  fodomr  8111  ssenen  8134  fi0  8326  cantnfp1  8578  cnfcomlem  8596  cardaleph  8912  cflim2  9085  axdc4lem  9277  fpwwe2lem12  9463  fpwwe2lem13  9464  rankcf  9599  inatsk  9600  ltrnq  9801  addclprlem1  9838  mulclprlem  9841  1idpr  9851  prlem936  9869  reclem3pr  9871  mulcmpblnrlem  9891  recexsrlem  9924  map2psrpr  9931  addid0  10450  nnnn0addcl  11323  zindd  11478  qaddcl  11804  qmulcl  11806  qreccl  11808  xaddnemnf  12067  xaddnepnf  12068  xaddcom  12071  xnegdi  12078  xaddass  12079  xpncan  12081  xleadd1a  12083  xlt2add  12090  rexmul  12101  xmulgt0  12113  xmulge0  12114  xmulasslem3  12116  xlemul1a  12118  xadddilem  12124  xadddi2  12127  modmuladd  12712  modm1p1mod0  12721  modfzo0difsn  12742  seqf1olem2  12841  expp1  12867  expneg  12868  expcllem  12871  mulexp  12899  expmul  12905  sqoddm1div8  13028  bcpasc  13108  hashrabsn01  13162  fseq1hash  13165  hashinfxadd  13174  hashfzo  13216  fnfz0hash  13230  ffzo0hash  13233  hashf1lem1  13239  hashge2el2dif  13262  brfi1indlem  13278  lsw0  13352  ccatval1  13361  ccatval2  13362  swrdval  13417  reuccats1  13480  splval  13502  repswswrd  13531  2cshwcshw  13571  s4dom  13664  wrdlen2i  13686  shftfn  13813  reim0b  13859  cjexp  13890  sqeqd  13906  fsumser  14461  sumsnf  14473  sumsn  14475  binomlem  14561  expcnv  14596  prodsn  14692  prodsnf  14694  bpolylem  14779  bpoly2  14788  bpoly3  14789  ef0lem  14809  dvdsnegb  14999  mod2eq1n2dvds  15071  m1expe  15091  m1expo  15092  m1exp1  15093  flodddiv4  15137  sadadd2lem2  15172  gcdabs  15250  bezoutr1  15282  dvdslcm  15311  lcmeq0  15313  lcmcl  15314  lcmabs  15318  lcmgcdlem  15319  lcmdvds  15321  lcmf0val  15335  lcmftp  15349  lcmfunsnlem2  15353  coprmdvdsOLD  15367  mulgcddvds  15369  divgcdcoprmex  15380  pcge0  15566  pcadd  15593  pcmpt2  15597  prmreclem4  15623  ramval  15712  ramcl  15733  fvprmselelfz  15748  fvprmselgcd1  15749  ressid2  15928  ressval2  15929  mrcmndind  17366  frmdval  17388  mgm2nsgrplem3  17407  mulgfval  17542  mulgnn0subcl  17554  mulgnn0z  17567  isga  17724  symgval  17799  symgextfve  17839  symgfixf1  17857  f1omvdco2  17868  psgnsn  17940  odid  17957  gexid  17996  frgpuptinv  18184  frgpup2  18189  dprdsn  18435  srgmulgass  18531  srgpcomp  18532  srgbinomlem4  18543  ringinvnzdiv  18593  f1rhm0to0  18740  f1rhm0to0ALT  18741  isabvd  18820  issrng  18850  lmodvsmmulgdi  18898  mptscmfsupp0  18928  lvecinv  19113  lspdisj2  19127  lspfixed  19128  lspexch  19129  sralem  19177  srasca  19181  sravsca  19182  sraip  19183  assamulgscmlem2  19349  mplval  19428  opsrval  19474  cply1mul  19664  gsummoncoe1  19674  evl1fval  19692  znval  19883  psgndiflemB  19946  isphl  19973  scmate  20316  scmatscm  20319  mdetdiagid  20406  mdetunilem7  20424  mdetuni0  20427  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  slesolinvbi  20487  cpmatacl  20521  cpmatinvcl  20522  pmatcollpw2lem  20582  monmatcollpw  20584  pmatcollpwfi  20587  mp2pm2mplem4  20614  pm2mp  20630  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmadumatpoly  20688  cayhamlem4  20693  cayleyhamilton0  20694  cayleyhamiltonALT  20696  indistopon  20805  0ntr  20875  pnrmopn  21147  reftr  21317  kgenval  21338  pt1hmeo  21609  fmval  21747  fmf  21749  istmd  21878  istgp  21881  tsmsval2  21933  isxmet2d  22132  xpsxmetlem  22184  xpsmet  22187  blfvalps  22188  tmsval  22286  isnlm  22479  nmoleub  22535  idnghm  22547  blssioo  22598  blcvx  22601  icccvx  22749  pcorevlem  22826  isclm  22864  caufval  23073  iscms  23142  mbfsup  23431  i1f1  23457  dvexp3  23741  rolle  23753  dvivth  23773  deg1add  23863  0dgr  24001  coefv0  24004  elqaalem2  24075  dvradcnv  24175  abelthlem8  24193  efper  24231  logtayl  24406  abscxpbnd  24494  relogbcxpb  24525  dcubic2  24571  rlimcnp2  24693  cvxcl  24711  zetacvg  24741  lgamgulmlem2  24756  vmaval  24839  chtub  24937  logexprlim  24950  dchrsum2  24993  sumdchr2  24995  bposlem2  25010  lgsdir  25057  lgsne0  25060  lgsdirnn0  25069  lgsdinn0  25070  lgsquadlem2  25106  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  dchrvmasum2if  25186  dchrvmasumiflem1  25190  rpvmasum2  25201  pntpbnd1  25275  ostth2lem4  25325  trgcgrg  25410  ax5seglem1  25808  ax5seglem2  25809  ax5seglem5  25813  usgr1vr  26147  cplgr2vpr  26329  cplgr3v  26331  cusgrrusgr  26477  wlklenvm1  26517  wlk0prc  26550  wlksoneq1eq2  26560  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  crctcshlem4  26712  crctcsh  26716  wlkiswwlks1  26753  wwlksnextbi  26789  wwlksnextwrd  26792  midwwlks2s3  26860  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2a4  26898  clwlkclwwlklem3  26902  clwwlkinwwlk  26905  clwwlksn2  26910  clwwlksf  26915  clwwlksf1  26917  wwlksext2clwwlk  26924  clwwisshclwws  26928  erclwwlkseqlen  26933  eleclclwwlksnlem2  26939  erclwwlksneqlen  26945  umgrhashecclwwlk  26955  eucrctshift  27103  eucrct2eupth  27105  fusgr2wsp2nb  27198  grpoidinvlem2  27359  vcz  27430  nvz  27524  lnon0  27653  ipasslem2  27687  htthlem  27774  hvpncan  27896  hiidge0  27955  normgt0  27984  hsn0elch  28105  shsel3  28174  spansneleq  28429  normcan  28435  h1datomi  28440  fh1  28477  spansncvi  28511  5oalem1  28513  5oalem3  28515  5oalem5  28517  3oalem2  28522  pjdsi  28571  kbpj  28815  0hmop  28842  0lnfn  28844  adj0  28853  nlelshi  28919  branmfn  28964  opsqrlem1  28999  hst1h  29086  mdsl0  29169  superpos  29213  sumdmdlem  29277  cdj3lem1  29293  xrpxdivcld  29643  2sqn0  29646  xrge0npcan  29694  resvid2  29828  resvval2  29829  esumsnf  30126  esummulc1  30143  measxun2  30273  omsmeas  30385  sibfof  30402  probun  30481  bnj517  30955  mrsubfval  31405  msrval  31435  subdivcomb2  31612  dfrdg2  31701  bj-bary1lem1  33161  rdgeqoa  33218  finxpreclem2  33227  finxpreclem3  33230  matunitlindflem1  33405  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem14  33423  poimirlem15  33424  poimirlem17  33426  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  mbfposadd  33457  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  ftc1anclem8  33492  areacirc  33505  ismtyval  33599  ismrer1  33637  grposnOLD  33681  rabeq12f  33965  csbeq12  33966  iuneq12f  33972  lsatcv1  34335  glbconN  34663  atltcvr  34721  3dim2  34754  islln2a  34803  2at0mat0  34811  islpln2a  34834  islvol2aN  34878  pmodlem2  35133  pmapjat1  35139  pcl0bN  35209  osumclN  35253  pexmidALTN  35264  lhp2at0nle  35321  4atexlemunv  35352  cdleme18b  35579  cdleme31sn1  35669  cdleme31sde  35673  cdleme31sn2  35677  ltrniotavalbN  35872  trljco  36028  cdlemh  36105  cdlemk40t  36206  cdlemk40f  36207  cdleml9  36272  dihmeetlem3N  36594  dochkrshp  36675  dihprrn  36715  dihjat1  36718  dvh3dim  36735  dochkrsm  36747  dochexmid  36757  lcfl7lem  36788  lcfl9a  36794  lclkrlem1  36795  mapdspex  36957  mapdindp2  37010  mapdh6dN  37028  hdmap1l6d  37103  hdmap11lem2  37134  hdmap14lem4a  37163  hdmapip0  37207  hlhilset  37226  jm2.26a  37567  radcnvrat  38513  sumsnd  39185  icccncfext  40100  fperdvper  40133  dvcosax  40141  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  volioc  40188  itgiccshift  40196  stoweidlem34  40251  dirkercncflem2  40321  fourierdlem32  40356  fourierdlem41  40365  fourierdlem48  40371  fourierdlem64  40387  fourierdlem73  40396  fourierdlem79  40402  fourierdlem82  40405  fourierdlem97  40420  fourierdlem101  40424  fourierdlem109  40432  fourierdlem111  40434  fouriersw  40448  elaa2  40451  etransclem24  40475  etransclem25  40476  etransclem46  40497  nnfoctbdjlem  40672  ismeannd  40684  fzopredsuc  41333  fmtnorec2lem  41454  2pwp1prmfmtno  41504  sfprmdvdsmersenne  41520  sgprmdvdsmersenne  41521  lighneallem2  41523  lighneallem3  41524  dfodd6  41550  dfeven4  41551  m1expevenALTV  41560  clintopval  41840  lmod0rng  41868  2zrngagrp  41943  rngcval  41962  ringcval  42008  dmmpt2ssx2  42115  zlmodzxzscm  42135  zlmodzxzadd  42136  domnmsuppn0  42150  rmsuppss  42151  scmsuppss  42153  ply1mulgsumlem4  42177  ldepsprlem  42261  lincresunit2  42267  m1modmmod  42316  nn0sumshdiglemB  42414  0setrec  42447