Theorem sylan9eq 2485

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426

This theorem is referenced by:  sylan9req  2486  sylan9eqr  2487  difeq12  3457  uneq12  3493  ineq12  3535  ifeq12  3794  ifbi  3798  preq12  3944  prprc  3975  preq12b  4036  opeq12  4049  opthwiener  4581  ordintdif  4755  xpeq12  4846  sosn  4895  nfimad  5166  coi2  5342  funimass1  5479  f1orescnv  5644  resdif  5649  fvmpt2  5769  fvmptnf  5779  oveq12  6089  cbvmpt2v  6155  ovmpt2g  6214  caofinvl  6336  eqopi  6599  fmpt2co  6645  supp0cosupp0  6717  rdgsucmptf  6870  frsucmpt  6879  abianfplem  6899  oevn0  6943  oa0r  6966  om1r  6970  oe1m  6972  omass  7007  oeoalem  7023  oeoa  7024  oeoe  7026  map0g  7240  xpcomco  7389  sbthlem4  7412  sbthlem5  7413  xpmapenlem  7466  phplem3  7480  phplem4  7481  unxpdomlem3  7507  funsnfsupp  7632  ordtypelem7  7726  cardennn  8141  dfac9  8293  cdaassen  8339  alephsing  8433  axcc3  8595  ac6num  8636  konigthlem  8720  canthp1lem2  8807  ordpipq  9098  ltrnq  9135  addclprlem2  9173  mulclprlem  9175  prlem934  9189  prlem936  9203  mulcmpblnrlem  9227  addcnsr  9289  mulcnsr  9290  axcnre  9318  recex  9955  uzindOLD  10723  rpnnen1lem3  10968  rpnnen1lem5  10970  xaddpnf1  11183  xaddpnf2  11184  xaddmnf1  11185  xaddmnf2  11186  rexadd  11189  xaddnemnf  11191  xaddnepnf  11192  xadddilem  11244  om2uzrani  11758  om2uzrdg  11762  seqf1olem2  11829  seqf1o  11830  modexp  11982  faclbnd4lem3  12054  hashunsng  12137  lsw1  12252  swrdfv  12303  swrdccat  12367  ccats1swrdeqbi  12372  revfv  12386  cshwsublen  12416  wrdlen2  12531  shftcan1  12555  remul2  12602  immul2  12609  sumss  13184  geomulcvg  13318  ef0lem  13346  efieq1re  13465  rpnnen2lem1  13479  ruclem3  13497  dvdsnegb  13532  dvdscmul  13541  dvds2ln  13545  dvds2add  13546  dvds2sub  13547  gcdn0val  13676  rpmulgcd  13721  odzval  13845  pcval  13893  pcmpt  13936  prmreclem4  13962  1arithlem2  13967  vdwlem8  14031  ramcl2lem  14052  ramtcl  14053  ramtub  14055  ramcl2  14059  ramcl  14072  setsval  14180  prfcl  14995  curf1cl  15020  curfcl  15024  hofcl  15051  yonedalem4c  15069  psssdm  15368  grplactval  15602  cntzval  15818  f1omvdco2  15933  pmtrfinv  15946  odlem2  16021  gexlem2  16060  lsmvalx  16117  efgtval  16199  efgredlema  16216  vrgpval  16243  cyggex  16353  gsumcom2  16440  dvdsrtr  16677  abvtrivd  16848  lmhmco  17045  reslmhm  17054  lvecinv  17115  mplmon2  17506  subrgasclcl  17512  coe1fv  17560  zrhmulg  17782  znzrhval  17820  ocvval  17933  mavmul0g  18205  1marepvmarrepid  18227  mdetunilem2  18260  gsummatr01lem3  18304  gsummatr01  18306  smadiadetlem3  18315  isopn3  18511  cnpval  18681  ptbasfi  18995  dfac14  19032  cnmptkk  19097  xkofvcn  19098  cnmptk1p  19099  cnmptk2  19100  xkocnv  19228  flfval  19404  ptcmplem3  19467  ptcmpg  19470  tmdmulg  19504  prdsxmslem2  19945  subgnm2  20061  nmoval  20135  fsum2cn  20288  pcovalg  20425  cphnm  20553  tchnmval  20585  ovolctb  20814  ioorcl  20898  uniioombllem2  20904  itg1addlem3  21017  itg1climres  21033  itg2uba  21062  itg2splitlem  21067  elcpn  21249  dvexp  21268  dvexp2  21269  rolle  21303  cmvth  21304  mvth  21305  dvlip  21306  dvlipcn  21307  dvlip2  21308  dveq0  21313  dv11cn  21314  lhop1lem  21326  lhop2  21328  lhop  21329  dvcvx  21333  ftc2ditglem  21358  itgsubstlem  21361  ig1pval  21528  elply2  21548  coeid2  21591  coemul  21603  taylthlem2  21723  ulmdvlem1  21749  mtest  21753  pserval2  21760  abelthlem1  21780  abelthlem3  21782  abelthlem8  21788  abelthlem9  21789  pige3  21863  0cxp  21995  leibpi  22221  mule1  22370  bposlem5  22511  lgsval3  22537  lgsdinn0  22563  dchrvmasumlem1  22628  dchrisum0flblem1  22641  rpvmasum2  22645  padicval  22750  axsegconlem1  22985  ax5seglem9  23005  axpasch  23009  axeuclidlem  23030  axcontlem2  23033  nbgraop  23157  nbgraop1  23158  constr1trl  23309  1pthon  23312  2pthlem2  23317  constr3pthlem3  23365  vdgrval  23388  grpoidinvlem4  23516  grposn  23524  grpoinvval  23534  grpodivval  23552  gxval  23567  gxnn0add  23583  subgoov  23614  ablosn  23656  ipval  23920  sspgval  23949  sspsval  23951  sspnval  23957  nmooval  23985  ipasslem1  24053  ipasslem4  24056  hial0  24326  hial02  24327  ocsh  24508  pjhval  24622  hosval  24966  homval  24967  hodval  24968  hfsval  24969  hfmval  24970  braval  25170  kbval  25180  eigvalval  25186  0hmop  25209  adj0  25220  lnopeq0i  25233  nmopcoi  25321  pjclem4  25425  pj3si  25433  hstoh  25458  strlem3a  25478  hstrlem3a  25486  mdexchi  25561  atcv0eq  25605  atcv1  25606  fpwrelmap  25857  measxun2  26477  measdivcstOLD  26491  measdivcst  26492  ddeval1  26503  ddeval0  26504  ballotlemfp1  26721  signswmnd  26805  signstfvneq0  26820  igamgam  26882  subfacp1lem3  26917  subfacp1lem5  26919  cvmlift2lem3  27041  relexp1  27179  relexpcnv  27181  relexpadd  27186  fprodss  27307  binomfallfaclem2  27389  wrecseq123  27564  altopthsn  27838  bpolylem  28037  mblfinlem2  28270  mblfinlem3  28271  mbfresfi  28279  itg2addnclem  28284  itg2addnc  28287  ftc1anclem5  28312  fnetr  28399  reftr  28402  fnejoin2  28431  isbnd3  28524  bndss  28526  ghomco  28589  pw2f1ocnv  29228  hbtlem7  29323  dvconstbi  29450  expgrowth  29451  addrfv  29567  subrfv  29568  mulvfv  29569  refsum2cnlem1  29601  afveu  29902  wwlktovf1  30095  ccatw2s1p1  30112  ccatw2s1p2  30113  wlkiswwlk2lem3  30170  wwlknred  30198  el2spthonot0  30233  clwwlkgt0  30277  clwlkisclwwlklem2a  30290  clwwlkf  30299  clwwlkext2edg  30307  wwlkext2clwwlk  30308  clwwisshclwwn  30315  erclwwlknsym  30343  erclwwlkntr  30344  wwlkextproplem2  30404  extwwlkfablem1  30510  numclwwlkovf2ex  30522  numclwlk1lem2f1  30530  numclwwlk5lem  30547  mpt2sn  30565  lmod0rng  30607  lincdifsn  30664  lcoel0  30668  islindeps2  30723  bnj1128  31680  lkrval  32303  pmapval  32971  polvalN  33119  watvalN  33207  ldilset  33323  ltrnset  33332  dilsetN  33367  trnsetN  33370  trlset  33375  trlval  33376  cdleme16b  33493  cdleme31fv1  33605  cdlemg1idlemN  33786  tgrpset  33959  tendoset  33973  erngset  34014  erngplus  34017  erngmul  34020  erngset-rN  34022  erngplus-rN  34025  dvaset  34219  dvaplusg  34223  dvamulr  34226  dvavadd  34229  dvavsca  34231  diafval  34246  dvhset  34296  dvhmulr  34301  dvhvadd  34307  dvhvsca  34316  docafvalN  34337  djafvalN  34349  dibfval  34356  dicfval  34390  dihfval  34446  dihval  34447  dihvalc  34448  dihvalb  34452  dochfval  34565  djhfval  34612  lcdval  34804  mapdfval  34842  mapdn0  34884  hvmapfval  34974  hdmap1fval  35012  hdmapfval  35045  hgmapfval  35104