Theorem sylan9eq 2504

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 2469	. 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 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2435

This theorem is referenced by:  sylan9req  2505  sylan9eqr  2506  difeq12  3602  uneq12  3638  ineq12  3680  ifeq12  3943  ifbi  3947  preq12  4096  prprc  4127  preq12b  4191  opeq12  4204  opthwiener  4739  ordintdif  4917  xpeq12  5008  sosn  5059  nfimad  5336  coi2  5514  funimass1  5651  f1orescnv  5821  resdif  5826  fvmpt2  5948  fvmptnf  5958  oveq12  6290  cbvmpt2v  6362  ovmpt2g  6422  caofinvl  6552  eqopi  6819  fmpt2co  6868  mpt2sn  6876  supp0cosupp0  6941  mpt2curryd  7000  fvmpt2curryd  7002  rdgsucmptf  7096  frsucmpt  7105  oevn0  7167  oa0r  7190  om1r  7194  oe1m  7196  omass  7231  oeoalem  7247  oeoa  7248  oeoe  7250  map0g  7460  xpcomco  7609  sbthlem4  7632  sbthlem5  7633  xpmapenlem  7686  phplem3  7700  phplem4  7701  unxpdomlem3  7728  funsnfsupp  7855  ordtypelem7  7952  cardennn  8367  dfac9  8519  cdaassen  8565  alephsing  8659  axcc3  8821  ac6num  8862  konigthlem  8946  canthp1lem2  9034  ordpipq  9323  ltrnq  9360  addclprlem2  9398  mulclprlem  9400  prlem934  9414  prlem936  9428  mulcmpblnrlem  9450  addcnsr  9515  mulcnsr  9516  axcnre  9544  recex  10187  uzindOLD  10963  rpnnen1lem3  11219  rpnnen1lem5  11221  xaddpnf1  11434  xaddpnf2  11435  xaddmnf1  11436  xaddmnf2  11437  rexadd  11440  xaddnemnf  11442  xaddnepnf  11443  xadddilem  11495  om2uzrani  12042  om2uzrdg  12046  seqf1olem2  12126  seqf1o  12127  modexp  12280  faclbnd4lem3  12352  hashunsng  12438  lsw1  12567  ccatw2s1p1  12619  ccatw2s1p2  12620  swrdfv  12630  swrdccat  12697  ccats1swrdeqbi  12702  revfv  12716  cshwsublen  12746  wrdlen2  12865  wwlktovf1  12874  shftcan1  12895  remul2  12942  immul2  12949  sumss  13525  geomulcvg  13664  ef0lem  13692  efieq1re  13811  rpnnen2lem1  13825  ruclem3  13843  dvdsnegb  13878  dvdscmul  13887  dvds2ln  13891  dvds2add  13892  dvds2sub  13893  gcdn0val  14025  rpmulgcd  14070  odzval  14195  pcval  14245  pcmpt  14288  prmreclem4  14314  1arithlem2  14319  vdwlem8  14383  ramcl2lem  14404  ramtcl  14405  ramtub  14407  ramcl2  14411  ramcl  14424  setsval  14533  prfcl  15346  curf1cl  15371  curfcl  15375  hofcl  15402  yonedalem4c  15420  psssdm  15720  grplactval  16011  cntzval  16233  f1omvdco2  16347  pmtrfinv  16360  odlem2  16437  gexlem2  16476  lsmvalx  16533  efgtval  16615  efgredlema  16632  vrgpval  16659  cyggex  16774  gsumcom2  16877  dvdsrtr  17175  abvtrivd  17363  lmhmco  17563  reslmhm  17572  lvecinv  17633  mplmon2  18032  subrgasclcl  18038  coe1fv  18119  coe1fzgsumdlem  18217  evl1gsumdlem  18266  zrhmulg  18420  znzrhval  18458  ocvval  18571  mat1dimscm  18850  dmatid  18870  scmatdmat  18890  mavmul0g  18928  1marepvmarrepid  18950  mdetunilem2  18988  gsummatr01lem3  19032  gsummatr01  19034  smadiadetlem3  19043  m2cpminvid2lem  19128  chpdmatlem2  19213  isopn3  19440  cnpval  19610  ptbasfi  19955  dfac14  19992  cnmptkk  20057  xkofvcn  20058  cnmptk1p  20059  cnmptk2  20060  xkocnv  20188  flfval  20364  ptcmplem3  20427  ptcmpg  20430  tmdmulg  20464  prdsxmslem2  20905  subgnm2  21021  nmoval  21095  fsum2cn  21248  pcovalg  21385  cphnm  21513  tchnmval  21545  ovolctb  21774  ioorcl  21859  uniioombllem2  21865  itg1addlem3  21978  itg1climres  21994  itg2uba  22023  itg2splitlem  22028  elcpn  22210  dvexp  22229  dvexp2  22230  rolle  22264  cmvth  22265  mvth  22266  dvlip  22267  dvlipcn  22268  dvlip2  22269  dveq0  22274  dv11cn  22275  lhop1lem  22287  lhop2  22289  lhop  22290  dvcvx  22294  ftc2ditglem  22319  itgsubstlem  22322  ig1pval  22446  elply2  22466  coeid2  22509  coemul  22521  taylthlem2  22641  ulmdvlem1  22667  mtest  22671  pserval2  22678  abelthlem1  22698  abelthlem3  22700  abelthlem8  22706  abelthlem9  22707  pige3  22782  0cxp  22919  leibpi  23145  mule1  23294  bposlem5  23435  lgsval3  23461  lgsdinn0  23487  dchrvmasumlem1  23552  dchrisum0flblem1  23565  rpvmasum2  23569  padicval  23674  axsegconlem1  24092  ax5seglem9  24112  axpasch  24116  axeuclidlem  24137  axcontlem2  24140  nbgraop  24295  nbgraop1  24297  constr1trl  24462  1pthon  24465  2pthlem2  24470  usgra2adedgwlkonALT  24488  constr3pthlem3  24529  wlkiswwlk2lem3  24565  wwlknred  24595  wwlkextproplem2  24614  clwwlkgt0  24643  clwlkisclwwlklem2a  24657  clwwlkf  24666  clwwlkext2edg  24674  wwlkext2clwwlk  24675  clwwisshclwwn  24680  erclwwlknsym  24698  erclwwlkntr  24699  el2spthonot0  24743  vdgrval  24768  extwwlkfablem1  24946  numclwwlkovf2ex  24958  numclwlk1lem2f1  24966  numclwwlk5lem  24983  grpoidinvlem4  25081  grposn  25089  grpoinvval  25099  grpodivval  25117  gxval  25132  gxnn0add  25148  subgoov  25179  ablosn  25221  ipval  25485  sspgval  25514  sspsval  25516  sspnval  25522  nmooval  25550  ipasslem1  25618  ipasslem4  25621  hial0  25891  hial02  25892  ocsh  26073  pjhval  26187  hosval  26531  homval  26532  hodval  26533  hfsval  26534  hfmval  26535  braval  26735  kbval  26745  eigvalval  26751  0hmop  26774  adj0  26785  lnopeq0i  26798  nmopcoi  26886  pjclem4  26990  pj3si  26998  hstoh  27023  strlem3a  27043  hstrlem3a  27051  mdexchi  27126  atcv0eq  27170  atcv1  27171  fpwrelmap  27428  measxun2  28054  measdivcstOLD  28068  measdivcst  28069  ddeval1  28079  ddeval0  28080  ballotlemfp1  28303  signswmnd  28387  signstfvneq0  28402  igamgam  28464  subfacp1lem3  28499  subfacp1lem5  28501  cvmlift2lem3  28623  msubco  28764  relexp1  28927  relexpcnv  28929  relexpadd  28934  fprodss  29055  binomfallfaclem2  29137  wrecseq123  29312  altopthsn  29586  bpolylem  29785  mblfinlem2  30027  mblfinlem3  30028  mbfresfi  30036  itg2addnclem  30041  itg2addnc  30044  ftc1anclem5  30069  fnetr  30144  fnejoin2  30162  isbnd3  30255  bndss  30257  ghomco  30320  pw2f1ocnv  30954  hbtlem7  31049  lcmn0val  31177  dvconstbi  31215  expgrowth  31216  addrfv  31332  subrfv  31333  mulvfv  31334  refsum2cnlem1  31366  limcperiod  31542  cncfiooiccre  31605  dvbdfbdioolem1  31629  itgioocnicc  31666  fourierdlem73  31851  fourierdlem82  31860  fourierdlem94  31872  fourierdlem103  31881  fourierdlem104  31882  fourierdlem113  31891  sqwvfoura  31900  afveu  32076  uhgrasiz  32232  rnghmval  32415  lmod0rng  32694  lmodvsmdi  32710  lincdifsn  32760  lcoel0  32764  islindeps2  32819  bnj1128  33779  lkrval  34553  pmapval  35221  polvalN  35369  watvalN  35457  ldilset  35573  ltrnset  35582  dilsetN  35618  trnsetN  35621  trlset  35626  trlval  35627  cdleme16b  35744  cdleme31fv1  35857  cdlemg1idlemN  36038  tgrpset  36211  tendoset  36225  erngset  36266  erngplus  36269  erngmul  36272  erngset-rN  36274  erngplus-rN  36277  dvaset  36471  dvaplusg  36475  dvamulr  36478  dvavadd  36481  dvavsca  36483  diafval  36498  dvhset  36548  dvhmulr  36553  dvhvadd  36559  dvhvsca  36568  docafvalN  36589  djafvalN  36601  dibfval  36608  dicfval  36642  dihfval  36698  dihval  36699  dihvalc  36700  dihvalb  36704  dochfval  36817  djhfval  36864  lcdval  37056  mapdfval  37094  mapdn0  37136  hvmapfval  37226  hdmap1fval  37264  hdmapfval  37297  hgmapfval  37356