Theorem sylan9eq 2495

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 2460	. 2 |- ( ( A = B /\ B = C ) -> A = C )
4	1, 2, 3	syl2an 477	1 |- ( ( ph /\ ps ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436

This theorem is referenced by:  sylan9req  2496  sylan9eqr  2497  difeq12  3490  uneq12  3526  ineq12  3568  ifeq12  3827  ifbi  3831  preq12  3977  prprc  4008  preq12b  4069  opeq12  4082  opthwiener  4614  ordintdif  4789  xpeq12  4880  sosn  4929  nfimad  5199  coi2  5375  funimass1  5512  f1orescnv  5677  resdif  5682  fvmpt2  5802  fvmptnf  5812  oveq12  6121  cbvmpt2v  6187  ovmpt2g  6246  caofinvl  6368  eqopi  6631  fmpt2co  6677  supp0cosupp0  6749  mpt2curryd  6809  fvmpt2curryd  6811  rdgsucmptf  6905  frsucmpt  6914  oevn0  6976  oa0r  6999  om1r  7003  oe1m  7005  omass  7040  oeoalem  7056  oeoa  7057  oeoe  7059  map0g  7273  xpcomco  7422  sbthlem4  7445  sbthlem5  7446  xpmapenlem  7499  phplem3  7513  phplem4  7514  unxpdomlem3  7540  funsnfsupp  7665  ordtypelem7  7759  cardennn  8174  dfac9  8326  cdaassen  8372  alephsing  8466  axcc3  8628  ac6num  8669  konigthlem  8753  canthp1lem2  8841  ordpipq  9132  ltrnq  9169  addclprlem2  9207  mulclprlem  9209  prlem934  9223  prlem936  9237  mulcmpblnrlem  9261  addcnsr  9323  mulcnsr  9324  axcnre  9352  recex  9989  uzindOLD  10757  rpnnen1lem3  11002  rpnnen1lem5  11004  xaddpnf1  11217  xaddpnf2  11218  xaddmnf1  11219  xaddmnf2  11220  rexadd  11223  xaddnemnf  11225  xaddnepnf  11226  xadddilem  11278  om2uzrani  11796  om2uzrdg  11800  seqf1olem2  11867  seqf1o  11868  modexp  12020  faclbnd4lem3  12092  hashunsng  12175  lsw1  12290  swrdfv  12341  swrdccat  12405  ccats1swrdeqbi  12410  revfv  12424  cshwsublen  12454  wrdlen2  12569  shftcan1  12593  remul2  12640  immul2  12647  sumss  13222  geomulcvg  13357  ef0lem  13385  efieq1re  13504  rpnnen2lem1  13518  ruclem3  13536  dvdsnegb  13571  dvdscmul  13580  dvds2ln  13584  dvds2add  13585  dvds2sub  13586  gcdn0val  13715  rpmulgcd  13760  odzval  13884  pcval  13932  pcmpt  13975  prmreclem4  14001  1arithlem2  14006  vdwlem8  14070  ramcl2lem  14091  ramtcl  14092  ramtub  14094  ramcl2  14098  ramcl  14111  setsval  14219  prfcl  15034  curf1cl  15059  curfcl  15063  hofcl  15090  yonedalem4c  15108  psssdm  15407  grplactval  15644  cntzval  15860  f1omvdco2  15975  pmtrfinv  15988  odlem2  16063  gexlem2  16102  lsmvalx  16159  efgtval  16241  efgredlema  16258  vrgpval  16285  cyggex  16395  gsumcom2  16489  dvdsrtr  16766  abvtrivd  16947  lmhmco  17146  reslmhm  17155  lvecinv  17216  mplmon2  17597  subrgasclcl  17603  coe1fv  17684  evl1gsumdlem  17812  zrhmulg  17963  znzrhval  18001  ocvval  18114  mavmul0g  18386  1marepvmarrepid  18408  mdetunilem2  18441  gsummatr01lem3  18485  gsummatr01  18487  smadiadetlem3  18496  isopn3  18692  cnpval  18862  ptbasfi  19176  dfac14  19213  cnmptkk  19278  xkofvcn  19279  cnmptk1p  19280  cnmptk2  19281  xkocnv  19409  flfval  19585  ptcmplem3  19648  ptcmpg  19651  tmdmulg  19685  prdsxmslem2  20126  subgnm2  20242  nmoval  20316  fsum2cn  20469  pcovalg  20606  cphnm  20734  tchnmval  20766  ovolctb  20995  ioorcl  21079  uniioombllem2  21085  itg1addlem3  21198  itg1climres  21214  itg2uba  21243  itg2splitlem  21248  elcpn  21430  dvexp  21449  dvexp2  21450  rolle  21484  cmvth  21485  mvth  21486  dvlip  21487  dvlipcn  21488  dvlip2  21489  dveq0  21494  dv11cn  21495  lhop1lem  21507  lhop2  21509  lhop  21510  dvcvx  21514  ftc2ditglem  21539  itgsubstlem  21542  ig1pval  21666  elply2  21686  coeid2  21729  coemul  21741  taylthlem2  21861  ulmdvlem1  21887  mtest  21891  pserval2  21898  abelthlem1  21918  abelthlem3  21920  abelthlem8  21926  abelthlem9  21927  pige3  22001  0cxp  22133  leibpi  22359  mule1  22508  bposlem5  22649  lgsval3  22675  lgsdinn0  22701  dchrvmasumlem1  22766  dchrisum0flblem1  22779  rpvmasum2  22783  padicval  22888  axsegconlem1  23185  ax5seglem9  23205  axpasch  23209  axeuclidlem  23230  axcontlem2  23233  nbgraop  23357  nbgraop1  23358  constr1trl  23509  1pthon  23512  2pthlem2  23517  constr3pthlem3  23565  vdgrval  23588  grpoidinvlem4  23716  grposn  23724  grpoinvval  23734  grpodivval  23752  gxval  23767  gxnn0add  23783  subgoov  23814  ablosn  23856  ipval  24120  sspgval  24149  sspsval  24151  sspnval  24157  nmooval  24185  ipasslem1  24253  ipasslem4  24256  hial0  24526  hial02  24527  ocsh  24708  pjhval  24822  hosval  25166  homval  25167  hodval  25168  hfsval  25169  hfmval  25170  braval  25370  kbval  25380  eigvalval  25386  0hmop  25409  adj0  25420  lnopeq0i  25433  nmopcoi  25521  pjclem4  25625  pj3si  25633  hstoh  25658  strlem3a  25678  hstrlem3a  25686  mdexchi  25761  atcv0eq  25805  atcv1  25806  fpwrelmap  26055  measxun2  26646  measdivcstOLD  26660  measdivcst  26661  ddeval1  26672  ddeval0  26673  ballotlemfp1  26896  signswmnd  26980  signstfvneq0  26995  igamgam  27057  subfacp1lem3  27092  subfacp1lem5  27094  cvmlift2lem3  27216  relexp1  27355  relexpcnv  27357  relexpadd  27362  fprodss  27483  binomfallfaclem2  27565  wrecseq123  27740  altopthsn  28014  bpolylem  28213  mblfinlem2  28455  mblfinlem3  28456  mbfresfi  28464  itg2addnclem  28469  itg2addnc  28472  ftc1anclem5  28497  fnetr  28584  reftr  28587  fnejoin2  28616  isbnd3  28709  bndss  28711  ghomco  28774  pw2f1ocnv  29412  hbtlem7  29507  dvconstbi  29634  expgrowth  29635  addrfv  29751  subrfv  29752  mulvfv  29753  refsum2cnlem1  29785  afveu  30085  wwlktovf1  30278  ccatw2s1p1  30295  ccatw2s1p2  30296  wlkiswwlk2lem3  30353  wwlknred  30381  el2spthonot0  30416  clwwlkgt0  30460  clwlkisclwwlklem2a  30473  clwwlkf  30482  clwwlkext2edg  30490  wwlkext2clwwlk  30491  clwwisshclwwn  30498  erclwwlknsym  30526  erclwwlkntr  30527  wwlkextproplem2  30587  extwwlkfablem1  30693  numclwwlkovf2ex  30705  numclwlk1lem2f1  30713  numclwwlk5lem  30730  mpt2sn  30750  lmod0rng  30809  lmodvsmdi  30845  coe1fzgsumdlem  30870  mat1dimscm  30910  dmatid  30913  scmatdmat  30922  scmatmulcl  30925  lincdifsn  30955  lcoel0  30959  islindeps2  31014  m2pminv2lem  31100  bnj1128  32077  lkrval  32829  pmapval  33497  polvalN  33645  watvalN  33733  ldilset  33849  ltrnset  33858  dilsetN  33893  trnsetN  33896  trlset  33901  trlval  33902  cdleme16b  34019  cdleme31fv1  34131  cdlemg1idlemN  34312  tgrpset  34485  tendoset  34499  erngset  34540  erngplus  34543  erngmul  34546  erngset-rN  34548  erngplus-rN  34551  dvaset  34745  dvaplusg  34749  dvamulr  34752  dvavadd  34755  dvavsca  34757  diafval  34772  dvhset  34822  dvhmulr  34827  dvhvadd  34833  dvhvsca  34842  docafvalN  34863  djafvalN  34875  dibfval  34882  dicfval  34916  dihfval  34972  dihval  34973  dihvalc  34974  dihvalb  34978  dochfval  35091  djhfval  35138  lcdval  35330  mapdfval  35368  mapdn0  35410  hvmapfval  35500  hdmap1fval  35538  hdmapfval  35571  hgmapfval  35630