Theorem sylan9eq 2443

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

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2374

This theorem is referenced by:  sylan9req  2444  sylan9eqr  2445  difeq12  3531  uneq12  3567  ineq12  3609  ifeq12  3874  ifbi  3878  preq12  4025  prprc  4056  preq12b  4120  opeq12  4133  opthwiener  4663  ordintdif  4841  xpeq12  4932  sosn  4983  nfimad  5258  coi2  5432  funimass1  5569  f1orescnv  5739  resdif  5744  fvmpt2  5865  fvmptnf  5875  oveq12  6205  cbvmpt2v  6276  ovmpt2g  6336  caofinvl  6466  eqopi  6733  fmpt2co  6782  mpt2sn  6790  supp0cosupp0  6857  mpt2curryd  6916  fvmpt2curryd  6918  rdgsucmptf  7012  frsucmpt  7021  oevn0  7083  oa0r  7106  om1r  7110  oe1m  7112  omass  7147  oeoalem  7163  oeoa  7164  oeoe  7166  map0g  7377  xpcomco  7526  sbthlem4  7549  sbthlem5  7550  xpmapenlem  7603  phplem3  7617  phplem4  7618  unxpdomlem3  7642  funsnfsupp  7768  ordtypelem7  7864  cardennn  8277  dfac9  8429  cdaassen  8475  alephsing  8569  axcc3  8731  ac6num  8772  konigthlem  8856  canthp1lem2  8942  ordpipq  9231  ltrnq  9268  addclprlem2  9306  mulclprlem  9308  prlem934  9322  prlem936  9336  mulcmpblnrlem  9358  addcnsr  9423  mulcnsr  9424  axcnre  9452  recex  10098  rpnnen1lem3  11129  rpnnen1lem5  11131  xaddpnf1  11346  xaddpnf2  11347  xaddmnf1  11348  xaddmnf2  11349  rexadd  11352  xaddnemnf  11354  xaddnepnf  11355  xadddilem  11407  om2uzrani  11966  om2uzrdg  11970  seqf1olem2  12050  seqf1o  12051  modexp  12203  faclbnd4lem3  12275  hashunsng  12363  lsw1  12496  swrdfv  12560  swrdccat  12629  ccats1swrdeqbi  12634  revfv  12648  cshwsublen  12678  wrdlen2  12797  wwlktovf1  12806  relexp0  12860  relexpcnv  12870  shftcan1  12918  remul2  12965  immul2  12972  sumss  13548  geomulcvg  13687  fprodss  13757  ef0lem  13816  efieq1re  13936  rpnnen2lem1  13950  ruclem3  13968  dvdsnegb  14003  dvdscmul  14012  dvds2ln  14016  dvds2add  14017  dvds2sub  14018  gcdn0val  14150  rpmulgcd  14195  odzval  14320  pcval  14370  pcmpt  14413  prmreclem4  14439  1arithlem2  14444  vdwlem8  14508  ramcl2lem  14529  ramtcl  14530  ramtub  14532  ramcl2  14536  ramcl  14549  setsval  14659  prfcl  15589  curf1cl  15614  curfcl  15618  hofcl  15645  yonedalem4c  15663  psssdm  15963  grplactval  16254  cntzval  16476  f1omvdco2  16590  pmtrfinv  16603  psgnunilem5  16636  odlem2  16680  gexlem2  16719  lsmvalx  16776  efgtval  16858  efgredlema  16875  vrgpval  16902  cyggex  17017  gsumcom2  17117  dvdsrtr  17414  abvtrivd  17602  lmhmco  17802  reslmhm  17811  lvecinv  17872  mplmon2  18271  subrgasclcl  18277  coe1fv  18358  coe1fzgsumdlem  18456  evl1gsumdlem  18505  zrhmulg  18640  znzrhval  18676  ocvval  18789  mat1dimscm  19062  dmatid  19082  scmatdmat  19102  mavmul0g  19140  1marepvmarrepid  19162  mdetunilem2  19200  gsummatr01lem3  19244  gsummatr01  19246  smadiadetlem3  19255  m2cpminvid2lem  19340  chpdmatlem2  19425  isopn3  19653  cnpval  19823  ptbasfi  20167  dfac14  20204  cnmptkk  20269  xkofvcn  20270  cnmptk1p  20271  cnmptk2  20272  xkocnv  20400  flfval  20576  ptcmplem3  20639  ptcmpg  20642  tmdmulg  20676  prdsxmslem2  21117  subgnm2  21233  nmoval  21307  fsum2cn  21460  pcovalg  21597  cphnm  21725  tchnmval  21757  ovolctb  21986  ioorcl  22071  uniioombllem2  22077  itg1addlem3  22190  itg1climres  22206  itg2uba  22235  itg2splitlem  22240  elcpn  22422  dvexp  22441  dvexp2  22442  rolle  22476  cmvth  22477  mvth  22478  dvlip  22479  dvlipcn  22480  dvlip2  22481  dveq0  22486  dv11cn  22487  lhop1lem  22499  lhop2  22501  lhop  22502  dvcvx  22506  ftc2ditglem  22531  itgsubstlem  22534  ig1pval  22658  elply2  22678  coeid2  22721  coemul  22734  taylthlem2  22854  ulmdvlem1  22880  mtest  22884  pserval2  22891  abelthlem1  22911  abelthlem3  22913  abelthlem8  22919  abelthlem9  22920  pige3  22995  0cxp  23134  leibpi  23389  mule1  23539  bposlem5  23680  lgsval3  23706  lgsdinn0  23732  dchrvmasumlem1  23797  dchrisum0flblem1  23810  rpvmasum2  23814  padicval  23919  axsegconlem1  24341  ax5seglem9  24361  axpasch  24365  axeuclidlem  24386  axcontlem2  24389  nbgraop  24544  nbgraop1  24546  constr1trl  24711  1pthon  24714  2pthlem2  24719  usgra2adedgwlkonALT  24737  constr3pthlem3  24778  wlkiswwlk2lem3  24814  wwlknred  24844  wwlkextproplem2  24863  clwwlkgt0  24892  clwlkisclwwlklem2a  24906  clwwlkf  24915  clwwlkext2edg  24923  wwlkext2clwwlk  24924  clwwisshclwwn  24929  erclwwlknsym  24947  erclwwlkntr  24948  el2spthonot0  24992  vdgrval  25017  extwwlkfablem1  25195  numclwwlkovf2ex  25207  numclwlk1lem2f1  25215  numclwwlk5lem  25232  grpoidinvlem4  25326  grposn  25334  grpoinvval  25344  grpodivval  25362  gxval  25377  gxnn0add  25393  subgoov  25424  ablosn  25466  ipval  25730  sspgval  25759  sspsval  25761  sspnval  25767  nmooval  25795  ipasslem1  25863  ipasslem4  25866  hial0  26136  hial02  26137  ocsh  26318  pjhval  26432  hosval  26775  homval  26776  hodval  26777  hfsval  26778  hfmval  26779  braval  26979  kbval  26989  eigvalval  26995  0hmop  27018  adj0  27029  lnopeq0i  27042  nmopcoi  27130  pjclem4  27234  pj3si  27242  hstoh  27267  strlem3a  27287  hstrlem3a  27295  mdexchi  27370  atcv0eq  27414  atcv1  27415  fpwrelmap  27706  measxun2  28337  measdivcstOLD  28351  measdivcst  28352  ddeval1  28362  ddeval0  28363  ballotlemfp1  28613  signswmnd  28697  signstfvneq0  28712  igamgam  28780  subfacp1lem3  28815  subfacp1lem5  28817  cvmlift2lem3  28939  msubco  29080  binomfallfaclem2  29328  wrecseq123  29502  altopthsn  29764  bpolylem  29963  mblfinlem2  30217  mblfinlem3  30218  mbfresfi  30226  itg2addnclem  30232  itg2addnc  30235  ftc1anclem5  30260  fnetr  30335  fnejoin2  30353  isbnd3  30446  bndss  30448  ghomco  30511  pw2f1ocnv  31145  hbtlem7  31242  lcmn0val  31369  dvconstbi  31407  expgrowth  31408  addrfv  31546  subrfv  31547  mulvfv  31548  refsum2cnlem1  31579  limcperiod  31800  cncfiooiccre  31864  dvbdfbdioolem1  31891  itgioocnicc  31942  fourierdlem73  32128  fourierdlem82  32137  fourierdlem94  32149  fourierdlem103  32158  fourierdlem104  32159  fourierdlem113  32168  sqwvfoura  32177  etransclem46  32229  afveu  32404  ccats1pfxeqbi  32606  uhgrasiz  32712  lmod0rng  32874  rnghmval  32897  lmodvsmdi  33175  lincdifsn  33225  lcoel0  33229  islindeps2  33284  blenn0  33394  nn0sumshdiglemA  33440  aacllem  33550  bnj1128  34393  lkrval  35226  pmapval  35894  polvalN  36042  watvalN  36130  ldilset  36246  ltrnset  36255  dilsetN  36291  trnsetN  36294  trlset  36299  trlval  36300  cdleme16b  36417  cdleme31fv1  36530  cdlemg1idlemN  36711  tgrpset  36884  tendoset  36898  erngset  36939  erngplus  36942  erngmul  36945  erngset-rN  36947  erngplus-rN  36950  dvaset  37144  dvaplusg  37148  dvamulr  37151  dvavadd  37154  dvavsca  37156  diafval  37171  dvhset  37221  dvhmulr  37226  dvhvadd  37232  dvhvsca  37241  docafvalN  37262  djafvalN  37274  dibfval  37281  dicfval  37315  dihfval  37371  dihval  37372  dihvalc  37373  dihvalb  37377  dochfval  37490  djhfval  37537  lcdval  37729  mapdfval  37767  mapdn0  37809  hvmapfval  37899  hdmap1fval  37937  hdmapfval  37970  hgmapfval  38029  relexp0a  38241