Theorem sylan9eq 2676

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

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  sylan9req  2677  sylan9eqr  2678  difeq12  3723  uneq12  3762  ineq12  3809  ssdifim  3862  ifeq12  4103  ifbi  4107  ifeq12da  4118  preq12  4270  prprc  4302  opeq12  4404  opthwiener  4976  xpeq12  5134  sosn  5188  nfimad  5475  coi2  5652  funprg  5940  funtpg  5942  funcnvtp  5951  funcnvqp  5952  funcnvqpOLD  5953  funimass1  5971  f1orescnv  6152  resdif  6157  fvmpt2  6291  fvmptnf  6302  fveqressseq  6355  oveq12  6659  cbvmpt2v  6735  ovmpt2g  6795  caofinvl  6924  eqopi  7202  el2mpt2csbcl  7250  fmpt2co  7260  mpt2sn  7268  supp0cosupp0  7334  mpt2curryd  7395  fvmpt2curryd  7397  wrecseq123  7408  rdgsucmptf  7524  frsucmpt  7533  oevn0  7595  oa0r  7618  om1r  7623  oe1m  7625  omass  7660  oeoalem  7676  oeoa  7677  oeoe  7679  map0g  7897  xpcomco  8050  sbthlem4  8073  sbthlem5  8074  xpmapenlem  8127  phplem3  8141  phplem4  8142  unxpdomlem3  8166  funsnfsupp  8299  ordtypelem7  8429  cardennn  8809  dfac9  8958  cdaassen  9004  alephsing  9098  axcc3  9260  ac6num  9301  konigthlem  9390  canthp1lem2  9475  ordpipq  9764  ltrnq  9801  addclprlem2  9839  mulclprlem  9841  prlem934  9855  prlem936  9869  mulcmpblnrlem  9891  addcnsr  9956  mulcnsr  9957  axcnre  9985  recex  10659  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  xaddpnf1  12057  xaddpnf2  12058  xaddmnf1  12059  xaddmnf2  12060  rexadd  12063  xnn0xaddcl  12066  xaddnemnf  12067  xaddnepnf  12068  xadddilem  12124  addmodlteq  12745  om2uzrani  12751  om2uzrdg  12755  seqf1olem2  12841  seqf1o  12842  modexp  12999  faclbnd4lem3  13082  hashunsng  13181  lsw1  13354  swrdfv  13424  swrdccat  13493  ccats1swrdeqbi  13498  revfv  13512  cshwsublen  13542  wrdlen2  13688  wrdl2exs2  13690  wwlktovf1  13700  relexp0  13763  relexpcnv  13775  shftcan1  13823  remul2  13870  immul2  13877  sumss  14455  geomulcvg  14607  fprodss  14678  binomfallfaclem2  14771  bpolylem  14779  ef0lem  14809  efieq1re  14929  rpnnen2lem1  14943  ruclem3  14962  dvdsnegb  14999  dvdscmul  15008  dvds2ln  15014  dvds2add  15015  dvds2sub  15016  gcdn0val  15220  rpmulgcd  15275  lcmn0val  15308  odzval  15496  pcval  15549  pcmpt  15596  prmreclem4  15623  1arithlem2  15628  vdwlem8  15692  ramcl2lem  15713  ramtcl  15714  ramtub  15716  ramcl2  15720  ramcl  15733  setsval  15888  prfcl  16843  curf1cl  16868  curfcl  16872  hofcl  16899  yonedalem4c  16917  psssdm  17216  grplactval  17517  cntzval  17754  f1omvdco2  17868  pmtrfinv  17881  psgnunilem5  17914  odlem2  17958  gexlem2  17997  lsmvalx  18054  efgtval  18136  efgredlema  18153  vrgpval  18180  cyggex  18299  gsumcom2  18374  dvdsrtr  18652  abvtrivd  18840  lmhmco  19043  reslmhm  19052  lvecinv  19113  mplmon2  19493  subrgasclcl  19499  coe1fv  19576  coe1fzgsumdlem  19671  evl1gsumdlem  19720  zrhmulg  19858  znzrhval  19895  ocvval  20011  mat1dimscm  20281  dmatid  20301  scmatdmat  20321  mavmul0g  20359  1marepvmarrepid  20381  mdetunilem2  20419  gsummatr01lem3  20463  gsummatr01  20465  smadiadetlem3  20474  m2cpminvid2lem  20559  chpdmatlem2  20644  isopn3  20870  cnpval  21040  ptbasfi  21384  dfac14  21421  cnmptkk  21486  xkofvcn  21487  cnmptk1p  21488  cnmptk2  21489  xkocnv  21617  flfval  21794  ptcmplem3  21858  ptcmpg  21861  tmdmulg  21896  prdsxmslem2  22334  subgnm2  22438  nmoval  22519  fsum2cn  22674  pcovalg  22812  isclmp  22897  cphnm  22993  tchnmval  23028  ovolctb  23258  ioorcl  23345  uniioombllem2  23351  itg1addlem3  23465  itg1climres  23481  itg2uba  23510  itg2splitlem  23515  elcpn  23697  dvexp  23716  dvexp2  23717  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlipcn  23757  dvlip2  23758  dveq0  23763  dv11cn  23764  lhop1lem  23776  lhop2  23778  lhop  23779  dvcvx  23783  ftc2ditglem  23808  itgsubstlem  23811  ig1pval  23932  elply2  23952  coeid2  23995  coemul  24008  taylthlem2  24128  ulmdvlem1  24154  mtest  24158  pserval2  24165  abelthlem1  24185  abelthlem3  24187  abelthlem8  24193  abelthlem9  24194  pige3  24269  0cxp  24412  leibpi  24669  igamgam  24775  mule1  24874  bposlem5  25013  lgsval3  25040  lgsdinn0  25070  dchrvmasumlem1  25184  dchrisum0flblem1  25197  rpvmasum2  25201  padicval  25306  axsegconlem1  25797  ax5seglem9  25817  axpasch  25821  axeuclidlem  25842  axcontlem2  25845  finsumvtxdg2ssteplem4  26444  usgr2wlkspthlem2  26654  crctcshlem4  26712  wwlknp  26734  wlkiswwlks2lem3  26757  wwlksnred  26787  wwlksnextproplem2  26805  wspthsnwspthsnon  26811  umgrwwlks2on  26850  clwlkclwwlklem2a  26899  clwwlksf  26915  clwwlksext2edg  26923  wwlksext2clwwlk  26924  clwwisshclwwsn  26929  erclwwlksnsym  26947  erclwwlksntr  26948  eupth2lem3lem3  27090  eucrct2eupth  27105  fusgreghash2wspv  27199  numclwwlkovf2ex  27219  numclwlk1lem2f1  27227  grpoidinvlem4  27361  grpoinvval  27377  grpodivval  27389  ipval  27558  sspgval  27584  sspsval  27586  sspnval  27592  nmooval  27618  ipasslem1  27686  ipasslem4  27689  hial0  27959  hial02  27960  ocsh  28142  pjhval  28256  hosval  28599  homval  28600  hodval  28601  hfsval  28602  hfmval  28603  braval  28803  kbval  28813  eigvalval  28819  0hmop  28842  adj0  28853  lnopeq0i  28866  nmopcoi  28954  pjclem4  29058  pj3si  29066  hstoh  29091  strlem3a  29111  hstrlem3a  29119  mdexchi  29194  atcv0eq  29238  atcv1  29239  fpwrelmap  29508  smatfval  29861  measxun2  30273  measdivcstOLD  30287  measdivcst  30288  ddeval1  30297  ddeval0  30298  ballotlemfp1  30553  signswmnd  30634  signstfvneq0  30649  ftc2re  30676  itgexpif  30684  bnj1128  31058  subfacp1lem3  31164  subfacp1lem5  31166  cvmlift2lem3  31287  msubco  31428  altopthsn  32068  fnetr  32346  fnejoin2  32364  bj-evalid  33028  finxpreclem3  33230  finxpreclem5  33232  finxpreclem6  33233  curf  33387  curunc  33391  matunitlindf  33407  poimirlem4  33413  poimirlem25  33434  mblfinlem2  33447  mblfinlem3  33448  mbfresfi  33456  itg2addnclem  33461  itg2addnc  33464  ftc1anclem5  33489  isbnd3  33583  bndss  33585  grposnOLD  33681  ghomco  33690  qseq12  34058  lkrval  34375  pmapval  35043  polvalN  35191  watvalN  35279  ldilset  35395  ltrnset  35404  dilsetN  35440  trnsetN  35443  trlset  35448  trlval  35449  cdleme16b  35566  cdleme31fv1  35679  cdlemg1idlemN  35860  tgrpset  36033  tendoset  36047  erngset  36088  erngplus  36091  erngmul  36094  erngset-rN  36096  erngplus-rN  36099  dvaset  36293  dvaplusg  36297  dvamulr  36300  dvavadd  36303  dvavsca  36305  diafval  36320  dvhset  36370  dvhmulr  36375  dvhvadd  36381  dvhvsca  36390  docafvalN  36411  djafvalN  36423  dibfval  36430  dicfval  36464  dihfval  36520  dihval  36521  dihvalc  36522  dihvalb  36526  dochfval  36639  djhfval  36686  lcdval  36878  mapdfval  36916  mapdn0  36958  hvmapfval  37048  hdmap1fval  37086  hdmapfval  37119  hgmapfval  37178  pw2f1ocnv  37604  hbtlem7  37695  relexp0a  38008  ntrclscls00  38364  dvconstbi  38533  expgrowth  38534  addrfv  38673  subrfv  38674  mulvfv  38675  refsum2cnlem1  39196  limcperiod  39860  cncfiooiccre  40108  dvbdfbdioolem1  40143  itgioocnicc  40193  fourierdlem73  40396  fourierdlem82  40405  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  sqwvfoura  40445  etransclem46  40497  nnfoctbdjlem  40672  ovn0  40780  smflim  40985  afveu  41233  ccats1pfxeqbi  41431  lighneallem3  41524  mogoldbblem  41629  sbgoldbwt  41665  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbnd  41697  lmod0rng  41868  rnghmval  41891  lmodvsmdi  42163  lincdifsn  42213  lcoel0  42217  islindeps2  42272  blenn0  42367  nn0sumshdiglemA  42413  aacllem  42547