Theorem sylan9eq 2800

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
sylan9eq.1	⊢ (𝜑 → 𝐴 = 𝐵)
sylan9eq.2	⊢ (𝜓 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sylan9eq	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sylan9eq.2	. 2 ⊢ (𝜓 → 𝐵 = 𝐶)
3		eqtr 2763	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 595	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  sylan9req  2801  sylan9eqr  2802  difeq12  4144  uneq12  4186  ineq12  4236  ssdifim  4292  ifeq12  4566  ifbi  4570  ifeq12da  4581  preq12  4760  prprc  4792  opeq12  4899  eqsnuniex  5379  opthwiener  5533  opthhausdorff0  5537  xpeq12  5725  sosn  5786  nfimad  6098  coi2  6294  funprg  6632  funtpg  6633  funcnvtp  6641  funcnvqp  6642  funimass1  6660  fimadmfoALT  6845  f1orescnv  6877  resdif  6883  fvmpt2  7040  fvmptnf  7051  fveqressseq  7113  oveq12  7457  cbvmpov  7545  ovmpog  7609  fvmpopr2d  7612  caofinvl  7745  eqopi  8066  el2mpocsbcl  8126  fmpoco  8136  mposn  8144  fsuppeqg  8217  supp0cosupp0  8249  imacosupp  8250  mpocurryd  8310  fvmpocurryd  8312  wrecseq123OLD  8356  rdgsucmptf  8484  frsucmpt  8494  oevn0  8571  oa0r  8594  om1r  8599  oe1m  8601  omass  8636  oeoalem  8652  oeoa  8653  oeoe  8655  qseq12  8824  map0g  8942  xpcomco  9128  sbthlem4  9152  sbthlem5  9153  xpmapenlem  9210  phplem2  9271  phplem3OLD  9282  phplem4OLD  9283  unxpdomlem3  9315  funsnfsupp  9461  ordtypelem7  9593  ttrcltr  9785  cardennn  10052  dfac9  10206  alephsing  10345  axcc3  10507  ac6num  10548  konigthlem  10637  canthp1lem2  10722  ordpipq  11011  ltrnq  11048  addclprlem2  11086  mulclprlem  11088  prlem934  11102  prlem936  11116  mulcmpblnrlem  11139  addcnsr  11204  mulcnsr  11205  axcnre  11233  recex  11922  rpnnen1lem3  13044  rpnnen1lem5  13046  xaddpnf1  13288  xaddpnf2  13289  xaddmnf1  13290  xaddmnf2  13291  rexadd  13294  xnn0xaddcl  13297  xaddnemnf  13298  xaddnepnf  13299  xadddilem  13356  addmodlteq  13997  om2uzrani  14003  om2uzrdg  14007  seqf1olem2  14093  seqf1o  14094  modexp  14287  faclbnd4lem3  14344  hashunsng  14441  hashwrdn  14595  lsw1  14615  swrdfv  14696  swrdccat  14783  ccats1pfxeqbi  14790  revfv  14811  cshwsublen  14844  wrdlen2  14993  wrdl2exs2  14995  wwlktovf1  15006  relexp0  15072  relexpcnv  15084  shftcan1  15132  remul2  15179  immul2  15186  sumss  15772  geomulcvg  15924  fprodss  15996  binomfallfaclem2  16088  bpolylem  16096  ef0lem  16126  efieq1re  16247  rpnnen2lem1  16262  ruclem3  16281  dvdsnegb  16322  dvdscmul  16331  dvds2ln  16337  dvds2add  16338  dvds2sub  16339  gcdn0val  16544  rpmulgcd  16604  lcmn0val  16642  odzval  16838  pcval  16891  pcmpt  16939  prmreclem4  16966  1arithlem2  16971  vdwlem8  17035  ramcl2lem  17056  ramtcl  17057  ramtub  17059  ramcl2  17063  ramcl  17076  setsval  17214  prfcl  18272  curf1cl  18298  curfcl  18302  hofcl  18329  yonedalem4c  18347  psssdm  18652  grplactval  19082  mulgnn0gsum  19120  cntzval  19361  f1omvdco2  19490  pmtrfinv  19503  psgnunilem5  19536  odlem2  19581  gexlem2  19624  lsmvalx  19681  efgtval  19765  efgredlema  19782  vrgpval  19809  cyggex  19940  gsumcom2  20017  fincygsubgodd  20156  dvdsrtr  20394  rnghmval  20466  abvtrivd  20855  lmhmco  21065  reslmhm  21074  lvecinv  21138  zrhmulg  21543  znzrhval  21588  ocvval  21708  mplmon2  22108  subrgasclcl  22114  coe1fv  22229  coe1fzgsumdlem  22328  evl1gsumdlem  22381  mat1dimscm  22502  dmatid  22522  scmatdmat  22542  mavmul0g  22580  1marepvmarrepid  22602  mdetunilem2  22640  gsummatr01lem3  22684  gsummatr01  22686  smadiadetlem3  22695  m2cpminvid2lem  22781  chpdmatlem2  22866  isopn3  23095  cnpval  23265  ptbasfi  23610  dfac14  23647  cnmptkk  23712  xkofvcn  23713  cnmptk1p  23714  cnmptk2  23715  xkocnv  23843  flfval  24019  ptcmplem3  24083  ptcmpg  24086  tmdmulg  24121  prdsxmslem2  24563  subgnm2  24668  nmoval  24757  fsum2cn  24914  pcovalg  25064  isclmp  25149  cphnm  25246  tcphnmval  25282  ovolctb  25544  ioorcl  25631  uniioombllem2  25637  itg1addlem3  25752  itg1climres  25769  itg2uba  25798  itg2splitlem  25803  elcpn  25990  dvexp  26011  dvexp2  26012  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlipcn  26053  dvlip2  26054  dveq0  26059  dv11cn  26060  lhop1lem  26072  lhop2  26074  lhop  26075  dvcvx  26079  ftc2ditglem  26106  itgsubstlem  26109  ig1pval  26235  elply2  26255  coeid2  26298  coemul  26311  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem1  26461  mtest  26465  pserval2  26472  abelthlem1  26493  abelthlem3  26495  abelthlem8  26501  abelthlem9  26502  pige3ALT  26580  0cxp  26726  leibpi  27003  igamgam  27110  mule1  27209  bposlem5  27350  lgsval3  27377  lgsdinn0  27407  dchrvmasumlem1  27557  dchrisum0flblem1  27570  rpvmasum2  27574  padicval  27679  abssid  28283  abssnid  28285  cutpw2  28435  axsegconlem1  28950  ax5seglem9  28970  axpasch  28974  axeuclidlem  28995  axcontlem2  28998  finsumvtxdg2ssteplem4  29584  usgr2wlkspthlem2  29794  crctcshlem4  29853  wwlknp  29876  wlkiswwlks2lem3  29904  wwlksnred  29925  wwlksnextproplem2  29943  umgrwwlks2on  29990  clwlkclwwlklem2a  30030  clwwisshclwwsn  30048  clwwlknlbonbgr1  30071  clwwlkn1loopb  30075  clwwlkf  30079  clwwlkext2edg  30088  wwlksext2clwwlk  30089  erclwwlknsym  30102  erclwwlkntr  30103  clwwlknon1  30129  clwwlknonex2  30141  eupth2lem3lem3  30262  eucrct2eupth  30277  fusgreghash2wspv  30367  2clwwlk2clwwlklem  30378  2clwwlk2clwwlk  30382  numclwwlk1lem2f1  30389  grpoidinvlem4  30539  grpoinvval  30555  grpodivval  30567  ipval  30735  sspgval  30761  sspsval  30763  sspnval  30769  nmooval  30795  ipasslem1  30863  ipasslem4  30866  hial0  31134  hial02  31135  ocsh  31315  pjhval  31429  hosval  31772  homval  31773  hodval  31774  hfsval  31775  hfmval  31776  braval  31976  kbval  31986  eigvalval  31992  0hmop  32015  adj0  32026  lnopeq0i  32039  nmopcoi  32127  pjclem4  32231  pj3si  32239  hstoh  32264  strlem3a  32284  hstrlem3a  32292  mdexchi  32367  atcv0eq  32411  atcv1  32412  fpwrelmap  32747  cycpmco2lem4  33122  cycpmco2lem5  33123  smatfval  33741  measxun2  34174  measdivcst  34188  measdivcstALTV  34189  ddeval1  34198  ddeval0  34199  ballotlemfp1  34456  signswmnd  34534  signstfvneq0  34549  signstfvc  34551  ftc2re  34575  itgexpif  34583  bnj1128  34966  subfacp1lem3  35150  subfacp1lem5  35152  cvmlift2lem3  35273  msubco  35499  altopthsn  35925  ditgeq12d  36188  fnetr  36317  fnejoin2  36335  bj-evalid  37042  finxpreclem3  37359  finxpreclem5  37361  finxpreclem6  37362  curf  37558  curunc  37562  matunitlindf  37578  poimirlem4  37584  poimirlem25  37605  mblfinlem2  37618  mblfinlem3  37619  mbfresfi  37626  itg2addnclem  37631  itg2addnc  37634  ftc1anclem5  37657  isbnd3  37744  bndss  37746  grposnOLD  37842  ghomco  37851  xrneq12  38339  lkrval  39044  pmapval  39714  polvalN  39862  watvalN  39950  ldilset  40066  ltrnset  40075  dilsetN  40110  trnsetN  40113  trlset  40118  trlval  40119  cdleme16b  40236  cdleme31fv1  40348  cdlemg1idlemN  40529  tgrpset  40702  tendoset  40716  erngset  40757  erngplus  40760  erngmul  40763  erngset-rN  40765  erngplus-rN  40768  dvaset  40962  dvaplusg  40966  dvamulr  40969  dvavadd  40972  dvavsca  40974  diafval  40988  dvhset  41038  dvhmulr  41043  dvhvadd  41049  dvhvsca  41058  docafvalN  41079  djafvalN  41091  dibfval  41098  dicfval  41132  dihfval  41188  dihval  41189  dihvalc  41190  dihvalb  41194  dochfval  41307  djhfval  41354  lcdval  41546  mapdfval  41584  mapdn0  41626  hvmapfval  41716  hdmap1fval  41753  hdmapfval  41784  hgmapfval  41843  fmpocos  42229  sn-it0e0  42391  zaddcomlem  42427  pw2f1ocnv  42994  hbtlem7  43082  relexp0a  43678  ntrclscls00  44028  dvconstbi  44303  expgrowth  44304  addrfv  44438  subrfv  44439  mulvfv  44440  refsum2cnlem1  44937  limcperiod  45549  cncfiooiccre  45816  dvbdfbdioolem1  45849  itgioocnicc  45898  fourierdlem73  46100  fourierdlem82  46109  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  sqwvfoura  46149  etransclem46  46201  nnfoctbdjlem  46376  ovn0  46487  smflim  46698  afveu  47068  afv2eu  47153  fvmptrabdm  47208  imasetpreimafvbijlemfo  47279  lighneallem3  47481  mogoldbblem  47594  fpprel2  47615  sbgoldbwt  47651  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbnd  47683  grimco  47764  lmod0rng  47952  lmodvsmdi  48107  lincdifsn  48153  lcoel0  48157  islindeps2  48212  blenn0  48307  nn0sumshdiglemA  48353  itcoval0mpt  48400  rrx2plordisom  48457  aacllem  48895