Theorem sylan9eq 2792

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  sylan9req  2793  sylan9eqr  2794  difeq12  4117  uneq12  4158  ineq12  4207  ssdifim  4262  ifeq12  4546  ifbi  4550  ifeq12da  4561  preq12  4739  prprc  4771  opeq12  4875  eqsnuniex  5359  opthwiener  5514  opthhausdorff0  5518  xpeq12  5701  sosn  5762  nfimad  6068  coi2  6262  funprg  6602  funtpg  6603  funcnvtp  6611  funcnvqp  6612  funimass1  6630  fimadmfoALT  6816  f1orescnv  6848  resdif  6854  fvmpt2  7009  fvmptnf  7020  fveqressseq  7081  oveq12  7420  cbvmpov  7506  ovmpog  7569  fvmpopr2d  7571  caofinvl  7702  eqopi  8013  el2mpocsbcl  8073  fmpoco  8083  mposn  8091  fsuppeqg  8163  supp0cosupp0  8195  imacosupp  8196  mpocurryd  8256  fvmpocurryd  8258  wrecseq123OLD  8302  rdgsucmptf  8430  frsucmpt  8440  oevn0  8517  oa0r  8540  om1r  8545  oe1m  8547  omass  8582  oeoalem  8598  oeoa  8599  oeoe  8601  qseq12  8763  map0g  8880  xpcomco  9064  sbthlem4  9088  sbthlem5  9089  xpmapenlem  9146  phplem2  9210  phplem3OLD  9221  phplem4OLD  9222  unxpdomlem3  9254  funsnfsupp  9389  ordtypelem7  9521  ttrcltr  9713  cardennn  9980  dfac9  10133  alephsing  10273  axcc3  10435  ac6num  10476  konigthlem  10565  canthp1lem2  10650  ordpipq  10939  ltrnq  10976  addclprlem2  11014  mulclprlem  11016  prlem934  11030  prlem936  11044  mulcmpblnrlem  11067  addcnsr  11132  mulcnsr  11133  axcnre  11161  recex  11848  rpnnen1lem3  12965  rpnnen1lem5  12967  xaddpnf1  13207  xaddpnf2  13208  xaddmnf1  13209  xaddmnf2  13210  rexadd  13213  xnn0xaddcl  13216  xaddnemnf  13217  xaddnepnf  13218  xadddilem  13275  addmodlteq  13913  om2uzrani  13919  om2uzrdg  13923  seqf1olem2  14010  seqf1o  14011  modexp  14203  faclbnd4lem3  14257  hashunsng  14354  hashwrdn  14499  lsw1  14519  swrdfv  14600  swrdccat  14687  ccats1pfxeqbi  14694  revfv  14715  cshwsublen  14748  wrdlen2  14897  wrdl2exs2  14899  wwlktovf1  14910  relexp0  14972  relexpcnv  14984  shftcan1  15032  remul2  15079  immul2  15086  sumss  15672  geomulcvg  15824  fprodss  15894  binomfallfaclem2  15986  bpolylem  15994  ef0lem  16024  efieq1re  16144  rpnnen2lem1  16159  ruclem3  16178  dvdsnegb  16219  dvdscmul  16228  dvds2ln  16234  dvds2add  16235  dvds2sub  16236  gcdn0val  16441  rpmulgcd  16500  lcmn0val  16534  odzval  16726  pcval  16779  pcmpt  16827  prmreclem4  16854  1arithlem2  16859  vdwlem8  16923  ramcl2lem  16944  ramtcl  16945  ramtub  16947  ramcl2  16951  ramcl  16964  setsval  17102  prfcl  18157  curf1cl  18183  curfcl  18187  hofcl  18214  yonedalem4c  18232  psssdm  18537  grplactval  18927  mulgnn0gsum  18962  cntzval  19187  f1omvdco2  19318  pmtrfinv  19331  psgnunilem5  19364  odlem2  19409  gexlem2  19452  lsmvalx  19509  efgtval  19593  efgredlema  19610  vrgpval  19637  cyggex  19768  gsumcom2  19845  fincygsubgodd  19984  dvdsrtr  20186  abvtrivd  20452  lmhmco  20659  reslmhm  20668  lvecinv  20732  zrhmulg  21065  znzrhval  21108  ocvval  21226  mplmon2  21628  subrgasclcl  21634  coe1fv  21736  coe1fzgsumdlem  21832  evl1gsumdlem  21882  mat1dimscm  21984  dmatid  22004  scmatdmat  22024  mavmul0g  22062  1marepvmarrepid  22084  mdetunilem2  22122  gsummatr01lem3  22166  gsummatr01  22168  smadiadetlem3  22177  m2cpminvid2lem  22263  chpdmatlem2  22348  isopn3  22577  cnpval  22747  ptbasfi  23092  dfac14  23129  cnmptkk  23194  xkofvcn  23195  cnmptk1p  23196  cnmptk2  23197  xkocnv  23325  flfval  23501  ptcmplem3  23565  ptcmpg  23568  tmdmulg  23603  prdsxmslem2  24045  subgnm2  24150  nmoval  24239  fsum2cn  24394  pcovalg  24535  isclmp  24620  cphnm  24717  tcphnmval  24753  ovolctb  25014  ioorcl  25101  uniioombllem2  25107  itg1addlem3  25222  itg1climres  25239  itg2uba  25268  itg2splitlem  25273  elcpn  25458  dvexp  25477  dvexp2  25478  rolle  25514  cmvth  25515  mvth  25516  dvlip  25517  dvlipcn  25518  dvlip2  25519  dveq0  25524  dv11cn  25525  lhop1lem  25537  lhop2  25539  lhop  25540  dvcvx  25544  ftc2ditglem  25569  itgsubstlem  25572  ig1pval  25697  elply2  25717  coeid2  25760  coemul  25773  taylthlem2  25893  ulmdvlem1  25919  mtest  25923  pserval2  25930  abelthlem1  25950  abelthlem3  25952  abelthlem8  25958  abelthlem9  25959  pige3ALT  26036  0cxp  26181  leibpi  26454  igamgam  26560  mule1  26659  bposlem5  26798  lgsval3  26825  lgsdinn0  26855  dchrvmasumlem1  27005  dchrisum0flblem1  27018  rpvmasum2  27022  padicval  27127  axsegconlem1  28213  ax5seglem9  28233  axpasch  28237  axeuclidlem  28258  axcontlem2  28261  finsumvtxdg2ssteplem4  28843  usgr2wlkspthlem2  29053  crctcshlem4  29112  wwlknp  29135  wlkiswwlks2lem3  29163  wwlksnred  29184  wwlksnextproplem2  29202  umgrwwlks2on  29249  clwlkclwwlklem2a  29289  clwwisshclwwsn  29307  clwwlknlbonbgr1  29330  clwwlkn1loopb  29334  clwwlkf  29338  clwwlkext2edg  29347  wwlksext2clwwlk  29348  erclwwlknsym  29361  erclwwlkntr  29362  clwwlknon1  29388  clwwlknonex2  29400  eupth2lem3lem3  29521  eucrct2eupth  29536  fusgreghash2wspv  29626  2clwwlk2clwwlklem  29637  2clwwlk2clwwlk  29641  numclwwlk1lem2f1  29648  grpoidinvlem4  29798  grpoinvval  29814  grpodivval  29826  ipval  29994  sspgval  30020  sspsval  30022  sspnval  30028  nmooval  30054  ipasslem1  30122  ipasslem4  30125  hial0  30393  hial02  30394  ocsh  30574  pjhval  30688  hosval  31031  homval  31032  hodval  31033  hfsval  31034  hfmval  31035  braval  31235  kbval  31245  eigvalval  31251  0hmop  31274  adj0  31285  lnopeq0i  31298  nmopcoi  31386  pjclem4  31490  pj3si  31498  hstoh  31523  strlem3a  31543  hstrlem3a  31551  mdexchi  31626  atcv0eq  31670  atcv1  31671  fpwrelmap  31996  cycpmco2lem4  32329  cycpmco2lem5  32330  smatfval  32844  measxun2  33277  measdivcst  33291  measdivcstALTV  33292  ddeval1  33301  ddeval0  33302  ballotlemfp1  33559  signswmnd  33637  signstfvneq0  33652  signstfvc  33654  ftc2re  33679  itgexpif  33687  bnj1128  34070  subfacp1lem3  34242  subfacp1lem5  34244  cvmlift2lem3  34365  msubco  34591  altopthsn  35002  gg-cmvth  35250  fnetr  35322  fnejoin2  35340  bj-evalid  36043  finxpreclem3  36360  finxpreclem5  36362  finxpreclem6  36363  curf  36552  curunc  36556  matunitlindf  36572  poimirlem4  36578  poimirlem25  36599  mblfinlem2  36612  mblfinlem3  36613  mbfresfi  36620  itg2addnclem  36625  itg2addnc  36628  ftc1anclem5  36651  isbnd3  36738  bndss  36740  grposnOLD  36836  ghomco  36845  xrneq12  37339  lkrval  38044  pmapval  38714  polvalN  38862  watvalN  38950  ldilset  39066  ltrnset  39075  dilsetN  39110  trnsetN  39113  trlset  39118  trlval  39119  cdleme16b  39236  cdleme31fv1  39348  cdlemg1idlemN  39529  tgrpset  39702  tendoset  39716  erngset  39757  erngplus  39760  erngmul  39763  erngset-rN  39765  erngplus-rN  39768  dvaset  39962  dvaplusg  39966  dvamulr  39969  dvavadd  39972  dvavsca  39974  diafval  39988  dvhset  40038  dvhmulr  40043  dvhvadd  40049  dvhvsca  40058  docafvalN  40079  djafvalN  40091  dibfval  40098  dicfval  40132  dihfval  40188  dihval  40189  dihvalc  40190  dihvalb  40194  dochfval  40307  djhfval  40354  lcdval  40546  mapdfval  40584  mapdn0  40626  hvmapfval  40716  hdmap1fval  40753  hdmapfval  40784  hgmapfval  40843  fmpocos  41142  sn-it0e0  41370  zaddcomlem  41406  pw2f1ocnv  41858  hbtlem7  41949  relexp0a  42549  ntrclscls00  42899  dvconstbi  43175  expgrowth  43176  addrfv  43310  subrfv  43311  mulvfv  43312  refsum2cnlem1  43803  limcperiod  44423  cncfiooiccre  44690  dvbdfbdioolem1  44723  itgioocnicc  44772  fourierdlem73  44974  fourierdlem82  44983  fourierdlem94  44995  fourierdlem103  45004  fourierdlem104  45005  fourierdlem113  45014  sqwvfoura  45023  etransclem46  45075  nnfoctbdjlem  45250  ovn0  45361  smflim  45572  afveu  45940  afv2eu  46025  fvmptrabdm  46080  imasetpreimafvbijlemfo  46152  lighneallem3  46354  mogoldbblem  46467  fpprel2  46488  sbgoldbwt  46524  nnsum4primeseven  46547  nnsum4primesevenALTV  46548  bgoldbtbnd  46556  lmod0rng  46721  rnghmval  46768  lmodvsmdi  47137  lincdifsn  47183  lcoel0  47187  islindeps2  47242  blenn0  47337  nn0sumshdiglemA  47383  itcoval0mpt  47430  rrx2plordisom  47487  aacllem  47926