Theorem sylan9eq 2817

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  sylan9req  2818  sylan9eqr  2819  difeq12  4075  uneq12  4116  ineq12  4167  ssdifim  4225  ifeq12  4499  ifbi  4503  ifeq12da  4514  preq12  4694  prprc  4726  opeq12  4833  eqsnuniex  5318  opthwiener  5483  opthhausdorff0  5487  xpeq12  5672  sosn  5734  nfimad  6058  coi2  6251  funprg  6575  funtpg  6576  funcnvtp  6584  funcnvqp  6585  funimass1  6603  fimadmfoALT  6789  f1orescnv  6822  resdif  6828  fvmpt2  6987  fvmptnf  6998  fveqressseq  7060  oveq12  7405  cbvmpov  7491  ovmpog  7555  fvmpopr2d  7558  caofinvl  7692  eqopi  8006  el2mpocsbcl  8064  fmpoco  8074  mposn  8082  fsuppeqg  8156  supp0cosupp0  8188  imacosupp  8189  mpocurryd  8249  fvmpocurryd  8251  rdgsucmptf  8399  frsucmpt  8409  oevn0  8484  oa0r  8507  om1r  8512  oe1m  8514  omass  8549  oeoalem  8566  oeoa  8567  oeoe  8569  qseq12  8743  map0g  8866  xpcomco  9039  sbthlem4  9062  sbthlem5  9063  xpmapenlem  9116  phplem2  9173  unxpdomlem3  9202  funsnfsupp  9338  ordtypelem7  9472  ttrcltr  9671  cardennn  9941  dfac9  10093  alephsing  10233  axcc3  10395  ac6num  10436  konigthlem  10526  canthp1lem2  10611  ordpipq  10900  ltrnq  10937  addclprlem2  10975  mulclprlem  10977  prlem934  10991  prlem936  11005  mulcmpblnrlem  11028  addcnsr  11093  mulcnsr  11094  axcnre  11122  recex  11819  rpnnen1lem3  12980  rpnnen1lem5  12982  xaddpnf1  13229  xaddpnf2  13230  xaddmnf1  13231  xaddmnf2  13232  rexadd  13235  xnn0xaddcl  13238  xaddnemnf  13239  xaddnepnf  13240  xadddilem  13297  addmodlteq  13959  om2uzrani  13965  om2uzrdg  13969  seqf1olem2  14055  seqf1o  14056  modexp  14251  faclbnd4lem3  14308  hashunsng  14405  hashwrdn  14560  lsw1  14580  swrdfv  14662  swrdccat  14748  ccats1pfxeqbi  14755  revfv  14776  cshwsublen  14809  wrdlen2  14957  wrdl2exs2  14959  wwlktovf1  14970  relexp0  15036  relexpcnv  15048  shftcan1  15096  remul2  15157  immul2  15164  sumss  15751  geomulcvg  15906  fprodss  15978  binomfallfaclem2  16070  bpolylem  16078  ef0lem  16108  efieq1re  16231  rpnnen2lem1  16246  ruclem3  16265  dvdsnegb  16307  dvdscmul  16316  dvds2ln  16323  dvds2add  16324  dvds2sub  16325  gcdn0val  16532  rpmulgcd  16591  lcmn0val  16629  odzval  16827  pcval  16880  pcmpt  16928  prmreclem4  16955  1arithlem2  16960  vdwlem8  17024  ramcl2lem  17045  ramtcl  17046  ramtub  17048  ramcl2  17052  ramcl  17065  setsval  17203  prfcl  18235  curf1cl  18260  curfcl  18264  hofcl  18291  yonedalem4c  18309  psssdm  18614  chneq12  18646  grplactval  19084  mulgnn0gsum  19122  cntzval  19361  f1omvdco2  19488  pmtrfinv  19501  psgnunilem5  19534  odlem2  19579  gexlem2  19622  lsmvalx  19679  efgtval  19763  efgredlema  19780  vrgpval  19807  cyggex  19938  gsumcom2  20015  fincygsubgodd  20154  dvdsrtr  20413  rnghmval  20485  abvtrivd  20878  lmhmco  21107  reslmhm  21116  lvecinv  21180  zrhmulg  21558  znzrhval  21595  ocvval  21716  mplmon2  22111  subrgasclcl  22117  coe1fv  22265  coe1fzgsumdlem  22363  evl1gsumdlem  22416  mat1dimscm  22532  dmatid  22552  scmatdmat  22572  mavmul0g  22610  1marepvmarrepid  22632  mdetunilem2  22670  gsummatr01lem3  22714  gsummatr01  22716  smadiadetlem3  22725  m2cpminvid2lem  22811  chpdmatlem2  22896  isopn3  23123  cnpval  23293  ptbasfi  23638  dfac14  23675  cnmptkk  23740  xkofvcn  23741  cnmptk1p  23742  cnmptk2  23743  xkocnv  23871  flfval  24047  ptcmplem3  24111  ptcmpg  24114  tmdmulg  24149  prdsxmslem2  24586  subgnm2  24691  nmoval  24772  fsum2cn  24930  pcovalg  25071  isclmp  25156  cphnm  25252  tcphnmval  25288  ovolctb  25549  ioorcl  25636  uniioombllem2  25642  itg1addlem3  25757  itg1climres  25773  itg2uba  25802  itg2splitlem  25807  elcpn  25993  dvexp  26012  dvexp2  26013  rolle  26049  cmvth  26050  mvth  26051  dvlip  26052  dvlipcn  26053  dvlip2  26054  dveq0  26059  dv11cn  26060  lhop1lem  26072  lhop2  26074  lhop  26075  dvcvx  26079  ftc2ditglem  26104  itgsubstlem  26107  ig1pval  26233  elply2  26253  coeid2  26296  coemul  26309  taylthlem2  26434  ulmdvlem1  26460  mtest  26464  pserval2  26471  abelthlem1  26491  abelthlem3  26493  abelthlem8  26499  abelthlem9  26500  pige3ALT  26582  0cxp  26728  leibpi  27004  igamgam  27110  mule1  27209  bposlem5  27349  lgsval3  27376  lgsdinn0  27406  dchrvmasumlem1  27556  dchrisum0flblem1  27569  rpvmasum2  27573  padicval  27678  abssid  28331  abssnid  28333  axsegconlem1  29115  ax5seglem9  29135  axpasch  29139  axeuclidlem  29160  axcontlem2  29163  finsumvtxdg2ssteplem4  29746  usgr2wlkspthlem2  29955  crctcshlem4  30017  wwlknp  30040  wlkiswwlks2lem3  30068  wwlksnred  30089  wwlksnextproplem2  30107  usgrwwlks2on  30155  umgrwwlks2on  30156  clwlkclwwlklem2a  30197  clwwisshclwwsn  30215  clwwlknlbonbgr1  30238  clwwlkn1loopb  30242  clwwlkf  30246  clwwlkext2edg  30255  wwlksext2clwwlk  30256  erclwwlknsym  30269  erclwwlkntr  30270  clwwlknon1  30296  clwwlknonex2  30308  eupth2lem3lem3  30429  eucrct2eupth  30444  fusgreghash2wspv  30534  2clwwlk2clwwlklem  30545  2clwwlk2clwwlk  30549  numclwwlk1lem2f1  30556  grpoidinvlem4  30707  grpoinvval  30723  grpodivval  30735  ipval  30903  sspgval  30929  sspsval  30931  sspnval  30937  nmooval  30963  ipasslem1  31031  ipasslem4  31034  hial0  31302  hial02  31303  ocsh  31483  pjhval  31597  hosval  31940  homval  31941  hodval  31942  hfsval  31943  hfmval  31944  braval  32144  kbval  32154  eigvalval  32160  0hmop  32183  adj0  32194  lnopeq0i  32207  nmopcoi  32295  pjclem4  32399  pj3si  32407  hstoh  32432  strlem3a  32452  hstrlem3a  32460  mdexchi  32535  atcv0eq  32579  atcv1  32580  fpwrelmap  32932  cycpmco2lem4  33306  cycpmco2lem5  33307  fxpgaval  33344  smatfval  34089  measxun2  34504  measdivcst  34518  measdivcstALTV  34519  ddeval1  34528  ddeval0  34529  ballotlemfp1  34786  signswmnd  34848  signstfvneq0  34863  signstfvc  34865  ftc2re  34889  itgexpif  34897  bnj1128  35282  subfacp1lem3  35529  subfacp1lem5  35531  cvmlift2lem3  35652  msubco  35878  altopthsn  36308  ditgeq12d  36579  fnetr  36708  fnejoin2  36726  ttcsntrsucg  36879  bj-evalid  37563  finxpreclem3  37884  finxpreclem5  37886  finxpreclem6  37887  curf  38094  curunc  38098  matunitlindf  38114  poimirlem4  38120  poimirlem25  38141  mblfinlem2  38154  mblfinlem3  38155  mbfresfi  38162  itg2addnclem  38167  itg2addnc  38170  ftc1anclem5  38193  isbnd3  38280  bndss  38282  grposnOLD  38378  ghomco  38387  xrneq12  38898  lkrval  39709  pmapval  40378  polvalN  40526  watvalN  40614  ldilset  40730  ltrnset  40739  dilsetN  40774  trnsetN  40777  trlset  40782  trlval  40783  cdleme16b  40900  cdleme31fv1  41012  cdlemg1idlemN  41193  tgrpset  41366  tendoset  41380  erngset  41421  erngplus  41424  erngmul  41427  erngset-rN  41429  erngplus-rN  41432  dvaset  41626  dvaplusg  41630  dvamulr  41633  dvavadd  41636  dvavsca  41638  diafval  41652  dvhset  41702  dvhmulr  41707  dvhvadd  41713  dvhvsca  41722  docafvalN  41743  djafvalN  41755  dibfval  41762  dicfval  41796  dihfval  41852  dihval  41853  dihvalc  41854  dihvalb  41858  dochfval  41971  djhfval  42018  lcdval  42210  mapdfval  42248  mapdn0  42290  hvmapfval  42380  hdmap1fval  42417  hdmapfval  42448  hgmapfval  42507  fmpocos  42849  sn-it0e0  43022  zaddcomlem  43082  pw2f1ocnv  43611  hbtlem7  43699  relexp0a  44289  ntrclscls00  44639  dvconstbi  44907  expgrowth  44908  addrfv  45041  subrfv  45042  mulvfv  45043  refsum2cnlem1  45614  limcperiod  46201  cncfiooiccre  46466  dvbdfbdioolem1  46499  itgioocnicc  46548  fourierdlem73  46750  fourierdlem82  46759  fourierdlem94  46771  fourierdlem103  46780  fourierdlem104  46781  fourierdlem113  46790  sqwvfoura  46799  etransclem46  46851  nnfoctbdjlem  47026  ovn0  47137  smflim  47348  afveu  47744  afv2eu  47829  fvmptrabdm  47884  imasetpreimafvbijlemfo  48008  lighneallem3  48213  ppivalnnprm  48231  mogoldbblem  48339  fpprel2  48360  sbgoldbwt  48396  nnsum4primeseven  48419  nnsum4primesevenALTV  48420  bgoldbtbnd  48428  grimco  48508  cycl3grtri  48566  lmod0rng  48848  lmodvsmdi  48998  lincdifsn  49043  lcoel0  49047  islindeps2  49102  blenn0  49192  nn0sumshdiglemA  49238  itcoval0mpt  49285  rrx2plordisom  49342  nelsubclem  49685  aacllem  50419