Theorem sylan9eq 2490

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
sylan9eq.1	|- ( ph -> A = B )
sylan9eq.2	|- ( ps -> B = C )

Assertion

Ref	Expression
sylan9eq	|- ( ( ph /\ ps ) -> A = C )

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 |- ( ph -> A = B )
2		sylan9eq.2	. 2 |- ( ps -> B = C )
3		eqtr 2455	. 2 |- ( ( A = B /\ B = C ) -> A = C )
4	1, 2, 3	syl2an 479	1 |- ( ( ph /\ ps ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421

This theorem is referenced by:  sylan9req  2491  sylan9eqr  2492  difeq12  3584  uneq12  3621  ineq12  3665  ifeq12  3932  ifbi  3936  preq12  4084  prprc  4115  preq12b  4179  opeq12  4192  opthwiener  4723  xpeq12  4873  sosn  4924  nfimad  5197  coi2  5372  ordintdif  5491  funimass1  5674  f1orescnv  5846  resdif  5851  fvmpt2  5973  fvmptnf  5983  oveq12  6314  cbvmpt2v  6385  ovmpt2g  6445  caofinvl  6572  eqopi  6841  fmpt2co  6890  mpt2sn  6898  supp0cosupp0  6965  mpt2curryd  7024  fvmpt2curryd  7026  wrecseq123  7037  rdgsucmptf  7154  frsucmpt  7163  oevn0  7225  oa0r  7248  om1r  7252  oe1m  7254  omass  7289  oeoalem  7305  oeoa  7306  oeoe  7308  map0g  7519  xpcomco  7668  sbthlem4  7691  sbthlem5  7692  xpmapenlem  7745  phplem3  7759  phplem4  7760  unxpdomlem3  7784  funsnfsupp  7913  ordtypelem7  8039  cardennn  8416  dfac9  8564  cdaassen  8610  alephsing  8704  axcc3  8866  ac6num  8907  konigthlem  8991  canthp1lem2  9077  ordpipq  9366  ltrnq  9403  addclprlem2  9441  mulclprlem  9443  prlem934  9457  prlem936  9471  mulcmpblnrlem  9493  addcnsr  9558  mulcnsr  9559  axcnre  9587  recex  10243  rpnnen1lem3  11292  rpnnen1lem5  11294  xaddpnf1  11519  xaddpnf2  11520  xaddmnf1  11521  xaddmnf2  11522  rexadd  11525  xaddnemnf  11527  xaddnepnf  11528  xadddilem  11580  om2uzrani  12163  om2uzrdg  12167  seqf1olem2  12250  seqf1o  12251  modexp  12404  faclbnd4lem3  12477  hashunsng  12568  lsw1  12701  swrdfv  12765  swrdccat  12834  ccats1swrdeqbi  12839  revfv  12853  cshwsublen  12883  wrdlen2  13002  wwlktovf1  13011  relexp0  13065  relexpcnv  13077  shftcan1  13125  remul2  13172  immul2  13179  sumss  13768  geomulcvg  13910  fprodss  13980  binomfallfaclem2  14071  bpolylem  14079  ef0lem  14111  efieq1re  14231  rpnnen2lem1  14245  ruclem3  14263  dvdsnegb  14298  dvdscmul  14307  dvds2ln  14311  dvds2add  14312  dvds2sub  14313  gcdn0val  14446  rpmulgcd  14494  lcmn0val  14525  odzval  14696  pcval  14748  pcmpt  14791  prmreclem4  14817  1arithlem2  14822  vdwlem8  14892  ramcl2lem  14916  ramcl2lemOLD  14917  ramtcl  14918  ramtclOLD  14919  ramtub  14922  ramtubOLD  14923  ramcl2  14927  ramcl2OLD  14928  ramcl  14941  setsval  15100  prfcl  16030  curf1cl  16055  curfcl  16059  hofcl  16086  yonedalem4c  16104  psssdm  16404  grplactval  16695  cntzval  16917  f1omvdco2  17031  pmtrfinv  17044  psgnunilem5  17077  odlem2  17121  gexlem2  17160  lsmvalx  17217  efgtval  17299  efgredlema  17316  vrgpval  17343  cyggex  17458  gsumcom2  17533  dvdsrtr  17806  abvtrivd  17994  lmhmco  18192  reslmhm  18201  lvecinv  18262  mplmon2  18642  subrgasclcl  18648  coe1fv  18725  coe1fzgsumdlem  18821  evl1gsumdlem  18870  zrhmulg  19003  znzrhval  19039  ocvval  19152  mat1dimscm  19422  dmatid  19442  scmatdmat  19462  mavmul0g  19500  1marepvmarrepid  19522  mdetunilem2  19560  gsummatr01lem3  19604  gsummatr01  19606  smadiadetlem3  19615  m2cpminvid2lem  19700  chpdmatlem2  19785  isopn3  20004  cnpval  20174  ptbasfi  20518  dfac14  20555  cnmptkk  20620  xkofvcn  20621  cnmptk1p  20622  cnmptk2  20623  xkocnv  20751  flfval  20927  ptcmplem3  20991  ptcmpg  20994  tmdmulg  21029  prdsxmslem2  21466  subgnm2  21564  nmoval  21638  fsum2cn  21790  pcovalg  21927  cphnm  22055  tchnmval  22087  ovolctb  22312  ioorcl  22397  ioorclOLD  22402  uniioombllem2  22408  uniioombllem2OLD  22409  itg1addlem3  22524  itg1climres  22540  itg2uba  22569  itg2splitlem  22574  elcpn  22756  dvexp  22775  dvexp2  22776  rolle  22810  cmvth  22811  mvth  22812  dvlip  22813  dvlipcn  22814  dvlip2  22815  dveq0  22820  dv11cn  22821  lhop1lem  22833  lhop2  22835  lhop  22836  dvcvx  22840  ftc2ditglem  22865  itgsubstlem  22868  ig1pval  22989  elply2  23009  coeid2  23052  coemul  23065  taylthlem2  23185  ulmdvlem1  23211  mtest  23215  pserval2  23222  abelthlem1  23242  abelthlem3  23244  abelthlem8  23250  abelthlem9  23251  pige3  23328  0cxp  23467  leibpi  23724  igamgam  23830  mule1  23929  bposlem5  24070  lgsval3  24096  lgsdinn0  24122  dchrvmasumlem1  24187  dchrisum0flblem1  24200  rpvmasum2  24204  padicval  24309  axsegconlem1  24784  ax5seglem9  24804  axpasch  24808  axeuclidlem  24829  axcontlem2  24832  nbgraop  24987  nbgraop1  24989  constr1trl  25154  1pthon  25157  2pthlem2  25162  usgra2adedgwlkonALT  25180  constr3pthlem3  25221  wlkiswwlk2lem3  25257  wwlknred  25287  wwlkextproplem2  25306  clwwlkgt0  25335  clwlkisclwwlklem2a  25349  clwwlkf  25358  clwwlkext2edg  25366  wwlkext2clwwlk  25367  clwwisshclwwn  25372  erclwwlknsym  25390  erclwwlkntr  25391  el2spthonot0  25435  vdgrval  25460  extwwlkfablem1  25638  numclwwlkovf2ex  25650  numclwlk1lem2f1  25658  numclwwlk5lem  25675  grpoidinvlem4  25771  grposn  25779  grpoinvval  25789  grpodivval  25807  gxval  25822  gxnn0add  25838  subgoov  25869  ablosn  25911  ipval  26175  sspgval  26204  sspsval  26206  sspnval  26212  nmooval  26240  ipasslem1  26308  ipasslem4  26311  hial0  26581  hial02  26582  ocsh  26762  pjhval  26876  hosval  27219  homval  27220  hodval  27221  hfsval  27222  hfmval  27223  braval  27423  kbval  27433  eigvalval  27439  0hmop  27462  adj0  27473  lnopeq0i  27486  nmopcoi  27574  pjclem4  27678  pj3si  27686  hstoh  27711  strlem3a  27731  hstrlem3a  27739  mdexchi  27814  atcv0eq  27858  atcv1  27859  fpwrelmap  28152  smatfval  28451  measxun2  28862  measdivcstOLD  28876  measdivcst  28877  ddeval1  28887  ddeval0  28888  ballotlemfp1  29141  signswmnd  29225  signstfvneq0  29240  bnj1128  29578  subfacp1lem3  29684  subfacp1lem5  29686  cvmlift2lem3  29807  msubco  29948  altopthsn  30504  fnetr  30783  fnejoin2  30801  poimirlem4  31638  poimirlem25  31659  mblfinlem2  31672  mblfinlem3  31673  mbfresfi  31681  itg2addnclem  31687  itg2addnc  31690  ftc1anclem5  31715  isbnd3  31810  bndss  31812  ghomco  31875  lkrval  32353  pmapval  33021  polvalN  33169  watvalN  33257  ldilset  33373  ltrnset  33382  dilsetN  33418  trnsetN  33421  trlset  33426  trlval  33427  cdleme16b  33544  cdleme31fv1  33657  cdlemg1idlemN  33838  tgrpset  34011  tendoset  34025  erngset  34066  erngplus  34069  erngmul  34072  erngset-rN  34074  erngplus-rN  34077  dvaset  34271  dvaplusg  34275  dvamulr  34278  dvavadd  34281  dvavsca  34283  diafval  34298  dvhset  34348  dvhmulr  34353  dvhvadd  34359  dvhvsca  34368  docafvalN  34389  djafvalN  34401  dibfval  34408  dicfval  34442  dihfval  34498  dihval  34499  dihvalc  34500  dihvalb  34504  dochfval  34617  djhfval  34664  lcdval  34856  mapdfval  34894  mapdn0  34936  hvmapfval  35026  hdmap1fval  35064  hdmapfval  35097  hgmapfval  35156  pw2f1ocnv  35588  hbtlem7  35680  relexp0a  35937  dvconstbi  36310  expgrowth  36311  addrfv  36449  subrfv  36450  mulvfv  36451  refsum2cnlem1  36988  limcperiod  37270  cncfiooiccre  37335  dvbdfbdioolem1  37362  itgioocnicc  37413  fourierdlem73  37601  fourierdlem82  37610  fourierdlem94  37622  fourierdlem103  37631  fourierdlem104  37632  fourierdlem113  37641  sqwvfoura  37650  etransclem46  37702  afveu  38035  bgoldbwt  38258  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  bgoldbtbnd  38284  ccats1pfxeqbi  38352  uhgrasiz  38454  lmod0rng  38616  rnghmval  38639  lmodvsmdi  38917  lincdifsn  38967  lcoel0  38971  islindeps2  39026  blenn0  39135  nn0sumshdiglemA  39181  aacllem  39291