Theorem sylan9eq 2876

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 2841	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 597	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  sylan9req  2877  sylan9eqr  2878  difeq12  4094  uneq12  4134  ineq12  4184  ssdifim  4239  ifeq12  4484  ifbi  4488  ifeq12da  4499  preq12  4671  prprc  4703  opeq12  4805  opthwiener  5404  opthhausdorff0  5408  xpeq12  5580  sosn  5638  nfimad  5938  coi2  6116  funprg  6408  funtpg  6409  funcnvtp  6417  funcnvqp  6418  funimass1  6436  fimadmfoALT  6601  f1orescnv  6630  resdif  6635  fvmpt2  6779  fvmptnf  6790  fveqressseq  6847  oveq12  7165  cbvmpov  7249  ovmpog  7309  caofinvl  7436  eqopi  7725  el2mpocsbcl  7780  fmpoco  7790  mposn  7798  supp0cosupp0  7872  supp0cosupp0OLD  7873  imacosupp  7874  mpocurryd  7935  fvmpocurryd  7937  wrecseq123  7948  rdgsucmptf  8064  frsucmpt  8073  oevn0  8140  oa0r  8163  om1r  8169  oe1m  8171  omass  8206  oeoalem  8222  oeoa  8223  oeoe  8225  qseq12  8347  map0g  8448  xpcomco  8607  sbthlem4  8630  sbthlem5  8631  xpmapenlem  8684  phplem3  8698  phplem4  8699  unxpdomlem3  8724  funsnfsupp  8857  ordtypelem7  8988  cardennn  9412  dfac9  9562  alephsing  9698  axcc3  9860  ac6num  9901  konigthlem  9990  canthp1lem2  10075  ordpipq  10364  ltrnq  10401  addclprlem2  10439  mulclprlem  10441  prlem934  10455  prlem936  10469  mulcmpblnrlem  10492  addcnsr  10557  mulcnsr  10558  axcnre  10586  recex  11272  rpnnen1lem3  12379  rpnnen1lem5  12381  xaddpnf1  12620  xaddpnf2  12621  xaddmnf1  12622  xaddmnf2  12623  rexadd  12626  xnn0xaddcl  12629  xaddnemnf  12630  xaddnepnf  12631  xadddilem  12688  addmodlteq  13315  om2uzrani  13321  om2uzrdg  13325  seqf1olem2  13411  seqf1o  13412  modexp  13600  faclbnd4lem3  13656  hashunsng  13754  hashwrdn  13898  lsw1  13919  swrdfv  14010  swrdccat  14097  ccats1pfxeqbi  14104  revfv  14125  cshwsublen  14158  wrdlen2  14306  wrdl2exs2  14308  wwlktovf1  14321  relexp0  14382  relexpcnv  14394  shftcan1  14442  remul2  14489  immul2  14496  sumss  15081  geomulcvg  15232  fprodss  15302  binomfallfaclem2  15394  bpolylem  15402  ef0lem  15432  efieq1re  15552  rpnnen2lem1  15567  ruclem3  15586  dvdsnegb  15627  dvdscmul  15636  dvds2ln  15642  dvds2add  15643  dvds2sub  15644  gcdn0val  15847  rpmulgcd  15906  lcmn0val  15939  odzval  16128  pcval  16181  pcmpt  16228  prmreclem4  16255  1arithlem2  16260  vdwlem8  16324  ramcl2lem  16345  ramtcl  16346  ramtub  16348  ramcl2  16352  ramcl  16365  setsval  16513  prfcl  17453  curf1cl  17478  curfcl  17482  hofcl  17509  yonedalem4c  17527  psssdm  17826  grplactval  18201  mulgnn0gsum  18234  cntzval  18451  f1omvdco2  18576  pmtrfinv  18589  psgnunilem5  18622  odlem2  18667  gexlem2  18707  lsmvalx  18764  efgtval  18849  efgredlema  18866  vrgpval  18893  cyggex  19018  gsumcom2  19095  fincygsubgodd  19234  dvdsrtr  19402  abvtrivd  19611  lmhmco  19815  reslmhm  19824  lvecinv  19885  mplmon2  20273  subrgasclcl  20279  coe1fv  20374  coe1fzgsumdlem  20469  evl1gsumdlem  20519  zrhmulg  20657  znzrhval  20693  ocvval  20811  mat1dimscm  21084  dmatid  21104  scmatdmat  21124  mavmul0g  21162  1marepvmarrepid  21184  mdetunilem2  21222  gsummatr01lem3  21266  gsummatr01  21268  smadiadetlem3  21277  m2cpminvid2lem  21362  chpdmatlem2  21447  isopn3  21674  cnpval  21844  ptbasfi  22189  dfac14  22226  cnmptkk  22291  xkofvcn  22292  cnmptk1p  22293  cnmptk2  22294  xkocnv  22422  flfval  22598  ptcmplem3  22662  ptcmpg  22665  tmdmulg  22700  prdsxmslem2  23139  subgnm2  23243  nmoval  23324  fsum2cn  23479  pcovalg  23616  isclmp  23701  cphnm  23797  tcphnmval  23832  ovolctb  24091  ioorcl  24178  uniioombllem2  24184  itg1addlem3  24299  itg1climres  24315  itg2uba  24344  itg2splitlem  24349  elcpn  24531  dvexp  24550  dvexp2  24551  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvlipcn  24591  dvlip2  24592  dveq0  24597  dv11cn  24598  lhop1lem  24610  lhop2  24612  lhop  24613  dvcvx  24617  ftc2ditglem  24642  itgsubstlem  24645  ig1pval  24766  elply2  24786  coeid2  24829  coemul  24842  taylthlem2  24962  ulmdvlem1  24988  mtest  24992  pserval2  24999  abelthlem1  25019  abelthlem3  25021  abelthlem8  25027  abelthlem9  25028  pige3ALT  25105  0cxp  25249  leibpi  25520  igamgam  25626  mule1  25725  bposlem5  25864  lgsval3  25891  lgsdinn0  25921  dchrvmasumlem1  26071  dchrisum0flblem1  26084  rpvmasum2  26088  padicval  26193  axsegconlem1  26703  ax5seglem9  26723  axpasch  26727  axeuclidlem  26748  axcontlem2  26751  finsumvtxdg2ssteplem4  27330  usgr2wlkspthlem2  27539  crctcshlem4  27598  wwlknp  27621  wlkiswwlks2lem3  27649  wwlksnred  27670  wwlksnextproplem2  27689  umgrwwlks2on  27736  clwlkclwwlklem2a  27776  clwwisshclwwsn  27794  clwwlknlbonbgr1  27817  clwwlkn1loopb  27821  clwwlkf  27826  clwwlkext2edg  27835  wwlksext2clwwlk  27836  erclwwlknsym  27849  erclwwlkntr  27850  clwwlknon1  27876  clwwlknonex2  27888  eupth2lem3lem3  28009  eucrct2eupth  28024  fusgreghash2wspv  28114  2clwwlk2clwwlklem  28125  2clwwlk2clwwlk  28129  numclwwlk1lem2f1  28136  grpoidinvlem4  28284  grpoinvval  28300  grpodivval  28312  ipval  28480  sspgval  28506  sspsval  28508  sspnval  28514  nmooval  28540  ipasslem1  28608  ipasslem4  28611  hial0  28879  hial02  28880  ocsh  29060  pjhval  29174  hosval  29517  homval  29518  hodval  29519  hfsval  29520  hfmval  29521  braval  29721  kbval  29731  eigvalval  29737  0hmop  29760  adj0  29771  lnopeq0i  29784  nmopcoi  29872  pjclem4  29976  pj3si  29984  hstoh  30009  strlem3a  30029  hstrlem3a  30037  mdexchi  30112  atcv0eq  30156  atcv1  30157  fpwrelmap  30469  cycpmco2lem4  30771  cycpmco2lem5  30772  smatfval  31060  measxun2  31469  measdivcst  31483  measdivcstALTV  31484  ddeval1  31493  ddeval0  31494  ballotlemfp1  31749  signswmnd  31827  signstfvneq0  31842  signstfvc  31844  ftc2re  31869  itgexpif  31877  bnj1128  32262  subfacp1lem3  32429  subfacp1lem5  32431  cvmlift2lem3  32552  msubco  32778  altopthsn  33422  fnetr  33699  fnejoin2  33717  bj-evalid  34370  finxpreclem3  34677  finxpreclem5  34679  finxpreclem6  34680  curf  34885  curunc  34889  matunitlindf  34905  poimirlem4  34911  poimirlem25  34932  mblfinlem2  34945  mblfinlem3  34946  mbfresfi  34953  itg2addnclem  34958  itg2addnc  34961  ftc1anclem5  34986  isbnd3  35077  bndss  35079  grposnOLD  35175  ghomco  35184  xrneq12  35650  lkrval  36239  pmapval  36908  polvalN  37056  watvalN  37144  ldilset  37260  ltrnset  37269  dilsetN  37304  trnsetN  37307  trlset  37312  trlval  37313  cdleme16b  37430  cdleme31fv1  37542  cdlemg1idlemN  37723  tgrpset  37896  tendoset  37910  erngset  37951  erngplus  37954  erngmul  37957  erngset-rN  37959  erngplus-rN  37962  dvaset  38156  dvaplusg  38160  dvamulr  38163  dvavadd  38166  dvavsca  38168  diafval  38182  dvhset  38232  dvhmulr  38237  dvhvadd  38243  dvhvsca  38252  docafvalN  38273  djafvalN  38285  dibfval  38292  dicfval  38326  dihfval  38382  dihval  38383  dihvalc  38384  dihvalb  38388  dochfval  38501  djhfval  38548  lcdval  38740  mapdfval  38778  mapdn0  38820  hvmapfval  38910  hdmap1fval  38947  hdmapfval  38978  hgmapfval  39037  pw2f1ocnv  39683  hbtlem7  39774  relexp0a  40110  ntrclscls00  40465  dvconstbi  40715  expgrowth  40716  addrfv  40850  subrfv  40851  mulvfv  40852  refsum2cnlem1  41343  limcperiod  41958  cncfiooiccre  42227  dvbdfbdioolem1  42262  itgioocnicc  42311  fourierdlem73  42513  fourierdlem82  42522  fourierdlem94  42534  fourierdlem103  42543  fourierdlem104  42544  fourierdlem113  42553  sqwvfoura  42562  etransclem46  42614  nnfoctbdjlem  42786  ovn0  42897  smflim  43102  afveu  43401  afv2eu  43486  fvmptrabdm  43541  imasetpreimafvbijlemfo  43614  lighneallem3  43821  mogoldbblem  43934  fpprel2  43955  sbgoldbwt  43991  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbnd  44023  lmod0rng  44188  rnghmval  44211  lmodvsmdi  44479  lincdifsn  44528  lcoel0  44532  islindeps2  44587  blenn0  44682  nn0sumshdiglemA  44728  rrx2plordisom  44759  aacllem  44951