Theorem sylan9eq 2789

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

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

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 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  sylan9req  2790  sylan9eqr  2791  difeq12  4071  uneq12  4113  ineq12  4165  ssdifim  4223  ifeq12  4496  ifbi  4500  ifeq12da  4511  preq12  4690  prprc  4722  opeq12  4829  eqsnuniex  5304  opthwiener  5460  opthhausdorff0  5464  xpeq12  5647  sosn  5709  nfimad  6026  coi2  6220  funprg  6544  funtpg  6545  funcnvtp  6553  funcnvqp  6554  funimass1  6572  fimadmfoALT  6755  f1orescnv  6787  resdif  6793  fvmpt2  6950  fvmptnf  6961  fveqressseq  7022  oveq12  7365  cbvmpov  7451  ovmpog  7515  fvmpopr2d  7518  caofinvl  7652  eqopi  7967  el2mpocsbcl  8025  fmpoco  8035  mposn  8043  fsuppeqg  8116  supp0cosupp0  8148  imacosupp  8149  mpocurryd  8209  fvmpocurryd  8211  rdgsucmptf  8357  frsucmpt  8367  oevn0  8440  oa0r  8463  om1r  8468  oe1m  8470  omass  8505  oeoalem  8522  oeoa  8523  oeoe  8525  qseq12  8697  map0g  8820  xpcomco  8993  sbthlem4  9016  sbthlem5  9017  xpmapenlem  9070  phplem2  9127  unxpdomlem3  9156  funsnfsupp  9293  ordtypelem7  9427  ttrcltr  9623  cardennn  9893  dfac9  10045  alephsing  10184  axcc3  10346  ac6num  10387  konigthlem  10477  canthp1lem2  10562  ordpipq  10851  ltrnq  10888  addclprlem2  10926  mulclprlem  10928  prlem934  10942  prlem936  10956  mulcmpblnrlem  10979  addcnsr  11044  mulcnsr  11045  axcnre  11073  recex  11767  rpnnen1lem3  12890  rpnnen1lem5  12892  xaddpnf1  13139  xaddpnf2  13140  xaddmnf1  13141  xaddmnf2  13142  rexadd  13145  xnn0xaddcl  13148  xaddnemnf  13149  xaddnepnf  13150  xadddilem  13207  addmodlteq  13867  om2uzrani  13873  om2uzrdg  13877  seqf1olem2  13963  seqf1o  13964  modexp  14159  faclbnd4lem3  14216  hashunsng  14313  hashwrdn  14468  lsw1  14488  swrdfv  14570  swrdccat  14656  ccats1pfxeqbi  14663  revfv  14684  cshwsublen  14717  wrdlen2  14865  wrdl2exs2  14867  wwlktovf1  14878  relexp0  14944  relexpcnv  14956  shftcan1  15004  remul2  15051  immul2  15058  sumss  15645  geomulcvg  15797  fprodss  15869  binomfallfaclem2  15961  bpolylem  15969  ef0lem  15999  efieq1re  16122  rpnnen2lem1  16137  ruclem3  16156  dvdsnegb  16198  dvdscmul  16207  dvds2ln  16214  dvds2add  16215  dvds2sub  16216  gcdn0val  16423  rpmulgcd  16482  lcmn0val  16520  odzval  16717  pcval  16770  pcmpt  16818  prmreclem4  16845  1arithlem2  16850  vdwlem8  16914  ramcl2lem  16935  ramtcl  16936  ramtub  16938  ramcl2  16942  ramcl  16955  setsval  17092  prfcl  18124  curf1cl  18149  curfcl  18153  hofcl  18180  yonedalem4c  18198  psssdm  18503  chneq12  18535  grplactval  18970  mulgnn0gsum  19008  cntzval  19248  f1omvdco2  19375  pmtrfinv  19388  psgnunilem5  19421  odlem2  19466  gexlem2  19509  lsmvalx  19566  efgtval  19650  efgredlema  19667  vrgpval  19694  cyggex  19825  gsumcom2  19902  fincygsubgodd  20041  dvdsrtr  20302  rnghmval  20374  abvtrivd  20763  lmhmco  20993  reslmhm  21002  lvecinv  21066  zrhmulg  21462  znzrhval  21499  ocvval  21620  mplmon2  22014  subrgasclcl  22020  coe1fv  22145  coe1fzgsumdlem  22245  evl1gsumdlem  22298  mat1dimscm  22417  dmatid  22437  scmatdmat  22457  mavmul0g  22495  1marepvmarrepid  22517  mdetunilem2  22555  gsummatr01lem3  22599  gsummatr01  22601  smadiadetlem3  22610  m2cpminvid2lem  22696  chpdmatlem2  22781  isopn3  23008  cnpval  23178  ptbasfi  23523  dfac14  23560  cnmptkk  23625  xkofvcn  23626  cnmptk1p  23627  cnmptk2  23628  xkocnv  23756  flfval  23932  ptcmplem3  23996  ptcmpg  23999  tmdmulg  24034  prdsxmslem2  24471  subgnm2  24576  nmoval  24657  fsum2cn  24816  pcovalg  24966  isclmp  25051  cphnm  25147  tcphnmval  25183  ovolctb  25445  ioorcl  25532  uniioombllem2  25538  itg1addlem3  25653  itg1climres  25669  itg2uba  25698  itg2splitlem  25703  elcpn  25890  dvexp  25911  dvexp2  25912  rolle  25948  cmvth  25949  cmvthOLD  25950  mvth  25951  dvlip  25952  dvlipcn  25953  dvlip2  25954  dveq0  25959  dv11cn  25960  lhop1lem  25972  lhop2  25974  lhop  25975  dvcvx  25979  ftc2ditglem  26006  itgsubstlem  26009  ig1pval  26135  elply2  26155  coeid2  26198  coemul  26211  taylthlem2  26336  taylthlem2OLD  26337  ulmdvlem1  26363  mtest  26367  pserval2  26374  abelthlem1  26395  abelthlem3  26397  abelthlem8  26403  abelthlem9  26404  pige3ALT  26483  0cxp  26629  leibpi  26906  igamgam  27013  mule1  27112  bposlem5  27253  lgsval3  27280  lgsdinn0  27310  dchrvmasumlem1  27460  dchrisum0flblem1  27473  rpvmasum2  27477  padicval  27582  abssid  28209  abssnid  28211  axsegconlem1  28939  ax5seglem9  28959  axpasch  28963  axeuclidlem  28984  axcontlem2  28987  finsumvtxdg2ssteplem4  29571  usgr2wlkspthlem2  29780  crctcshlem4  29842  wwlknp  29865  wlkiswwlks2lem3  29893  wwlksnred  29914  wwlksnextproplem2  29932  usgrwwlks2on  29980  umgrwwlks2on  29981  clwlkclwwlklem2a  30022  clwwisshclwwsn  30040  clwwlknlbonbgr1  30063  clwwlkn1loopb  30067  clwwlkf  30071  clwwlkext2edg  30080  wwlksext2clwwlk  30081  erclwwlknsym  30094  erclwwlkntr  30095  clwwlknon1  30121  clwwlknonex2  30133  eupth2lem3lem3  30254  eucrct2eupth  30269  fusgreghash2wspv  30359  2clwwlk2clwwlklem  30370  2clwwlk2clwwlk  30374  numclwwlk1lem2f1  30381  grpoidinvlem4  30531  grpoinvval  30547  grpodivval  30559  ipval  30727  sspgval  30753  sspsval  30755  sspnval  30761  nmooval  30787  ipasslem1  30855  ipasslem4  30858  hial0  31126  hial02  31127  ocsh  31307  pjhval  31421  hosval  31764  homval  31765  hodval  31766  hfsval  31767  hfmval  31768  braval  31968  kbval  31978  eigvalval  31984  0hmop  32007  adj0  32018  lnopeq0i  32031  nmopcoi  32119  pjclem4  32223  pj3si  32231  hstoh  32256  strlem3a  32276  hstrlem3a  32284  mdexchi  32359  atcv0eq  32403  atcv1  32404  fpwrelmap  32761  cycpmco2lem4  33160  cycpmco2lem5  33161  fxpgaval  33198  smatfval  33901  measxun2  34316  measdivcst  34330  measdivcstALTV  34331  ddeval1  34340  ddeval0  34341  ballotlemfp1  34598  signswmnd  34663  signstfvneq0  34678  signstfvc  34680  ftc2re  34704  itgexpif  34712  bnj1128  35095  subfacp1lem3  35325  subfacp1lem5  35327  cvmlift2lem3  35448  msubco  35674  altopthsn  36104  ditgeq12d  36365  fnetr  36494  fnejoin2  36512  bj-evalid  37220  finxpreclem3  37537  finxpreclem5  37539  finxpreclem6  37540  curf  37738  curunc  37742  matunitlindf  37758  poimirlem4  37764  poimirlem25  37785  mblfinlem2  37798  mblfinlem3  37799  mbfresfi  37806  itg2addnclem  37811  itg2addnc  37814  ftc1anclem5  37837  isbnd3  37924  bndss  37926  grposnOLD  38022  ghomco  38031  xrneq12  38526  lkrval  39287  pmapval  39956  polvalN  40104  watvalN  40192  ldilset  40308  ltrnset  40317  dilsetN  40352  trnsetN  40355  trlset  40360  trlval  40361  cdleme16b  40478  cdleme31fv1  40590  cdlemg1idlemN  40771  tgrpset  40944  tendoset  40958  erngset  40999  erngplus  41002  erngmul  41005  erngset-rN  41007  erngplus-rN  41010  dvaset  41204  dvaplusg  41208  dvamulr  41211  dvavadd  41214  dvavsca  41216  diafval  41230  dvhset  41280  dvhmulr  41285  dvhvadd  41291  dvhvsca  41300  docafvalN  41321  djafvalN  41333  dibfval  41340  dicfval  41374  dihfval  41430  dihval  41431  dihvalc  41432  dihvalb  41436  dochfval  41549  djhfval  41596  lcdval  41788  mapdfval  41826  mapdn0  41868  hvmapfval  41958  hdmap1fval  41995  hdmapfval  42026  hgmapfval  42085  fmpocos  42432  sn-it0e0  42613  zaddcomlem  42660  pw2f1ocnv  43221  hbtlem7  43309  relexp0a  43899  ntrclscls00  44249  dvconstbi  44517  expgrowth  44518  addrfv  44651  subrfv  44652  mulvfv  44653  refsum2cnlem1  45224  limcperiod  45816  cncfiooiccre  46081  dvbdfbdioolem1  46114  itgioocnicc  46163  fourierdlem73  46365  fourierdlem82  46374  fourierdlem94  46386  fourierdlem103  46395  fourierdlem104  46396  fourierdlem113  46405  sqwvfoura  46414  etransclem46  46466  nnfoctbdjlem  46641  ovn0  46752  smflim  46963  afveu  47341  afv2eu  47426  fvmptrabdm  47481  imasetpreimafvbijlemfo  47593  lighneallem3  47795  mogoldbblem  47908  fpprel2  47929  sbgoldbwt  47965  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  bgoldbtbnd  47997  grimco  48077  cycl3grtri  48135  lmod0rng  48417  lmodvsmdi  48567  lincdifsn  48612  lcoel0  48616  islindeps2  48671  blenn0  48761  nn0sumshdiglemA  48807  itcoval0mpt  48854  rrx2plordisom  48911  nelsubclem  49254  aacllem  49988