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

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  sylan9req  2793  sylan9eqr  2794  difeq12  4062  uneq12  4104  ineq12  4156  ssdifim  4214  ifeq12  4486  ifbi  4490  ifeq12da  4501  preq12  4680  prprc  4712  opeq12  4819  eqsnuniex  5299  opthwiener  5463  opthhausdorff0  5467  xpeq12  5650  sosn  5712  nfimad  6029  coi2  6223  funprg  6547  funtpg  6548  funcnvtp  6556  funcnvqp  6557  funimass1  6575  fimadmfoALT  6758  f1orescnv  6790  resdif  6796  fvmpt2  6954  fvmptnf  6965  fveqressseq  7026  oveq12  7370  cbvmpov  7456  ovmpog  7520  fvmpopr2d  7523  caofinvl  7657  eqopi  7972  el2mpocsbcl  8029  fmpoco  8039  mposn  8047  fsuppeqg  8120  supp0cosupp0  8152  imacosupp  8153  mpocurryd  8213  fvmpocurryd  8215  rdgsucmptf  8361  frsucmpt  8371  oevn0  8444  oa0r  8467  om1r  8472  oe1m  8474  omass  8509  oeoalem  8526  oeoa  8527  oeoe  8529  qseq12  8702  map0g  8826  xpcomco  8999  sbthlem4  9022  sbthlem5  9023  xpmapenlem  9076  phplem2  9133  unxpdomlem3  9162  funsnfsupp  9299  ordtypelem7  9433  ttrcltr  9631  cardennn  9901  dfac9  10053  alephsing  10192  axcc3  10354  ac6num  10395  konigthlem  10485  canthp1lem2  10570  ordpipq  10859  ltrnq  10896  addclprlem2  10934  mulclprlem  10936  prlem934  10950  prlem936  10964  mulcmpblnrlem  10987  addcnsr  11052  mulcnsr  11053  axcnre  11081  recex  11776  rpnnen1lem3  12923  rpnnen1lem5  12925  xaddpnf1  13172  xaddpnf2  13173  xaddmnf1  13174  xaddmnf2  13175  rexadd  13178  xnn0xaddcl  13181  xaddnemnf  13182  xaddnepnf  13183  xadddilem  13240  addmodlteq  13902  om2uzrani  13908  om2uzrdg  13912  seqf1olem2  13998  seqf1o  13999  modexp  14194  faclbnd4lem3  14251  hashunsng  14348  hashwrdn  14503  lsw1  14523  swrdfv  14605  swrdccat  14691  ccats1pfxeqbi  14698  revfv  14719  cshwsublen  14752  wrdlen2  14900  wrdl2exs2  14902  wwlktovf1  14913  relexp0  14979  relexpcnv  14991  shftcan1  15039  remul2  15086  immul2  15093  sumss  15680  geomulcvg  15835  fprodss  15907  binomfallfaclem2  15999  bpolylem  16007  ef0lem  16037  efieq1re  16160  rpnnen2lem1  16175  ruclem3  16194  dvdsnegb  16236  dvdscmul  16245  dvds2ln  16252  dvds2add  16253  dvds2sub  16254  gcdn0val  16461  rpmulgcd  16520  lcmn0val  16558  odzval  16756  pcval  16809  pcmpt  16857  prmreclem4  16884  1arithlem2  16889  vdwlem8  16953  ramcl2lem  16974  ramtcl  16975  ramtub  16977  ramcl2  16981  ramcl  16994  setsval  17131  prfcl  18163  curf1cl  18188  curfcl  18192  hofcl  18219  yonedalem4c  18237  psssdm  18542  chneq12  18574  grplactval  19012  mulgnn0gsum  19050  cntzval  19290  f1omvdco2  19417  pmtrfinv  19430  psgnunilem5  19463  odlem2  19508  gexlem2  19551  lsmvalx  19608  efgtval  19692  efgredlema  19709  vrgpval  19736  cyggex  19867  gsumcom2  19944  fincygsubgodd  20083  dvdsrtr  20342  rnghmval  20414  abvtrivd  20803  lmhmco  21033  reslmhm  21042  lvecinv  21106  zrhmulg  21502  znzrhval  21539  ocvval  21660  mplmon2  22052  subrgasclcl  22058  coe1fv  22183  coe1fzgsumdlem  22281  evl1gsumdlem  22334  mat1dimscm  22453  dmatid  22473  scmatdmat  22493  mavmul0g  22531  1marepvmarrepid  22553  mdetunilem2  22591  gsummatr01lem3  22635  gsummatr01  22637  smadiadetlem3  22646  m2cpminvid2lem  22732  chpdmatlem2  22817  isopn3  23044  cnpval  23214  ptbasfi  23559  dfac14  23596  cnmptkk  23661  xkofvcn  23662  cnmptk1p  23663  cnmptk2  23664  xkocnv  23792  flfval  23968  ptcmplem3  24032  ptcmpg  24035  tmdmulg  24070  prdsxmslem2  24507  subgnm2  24612  nmoval  24693  fsum2cn  24851  pcovalg  24992  isclmp  25077  cphnm  25173  tcphnmval  25209  ovolctb  25470  ioorcl  25557  uniioombllem2  25563  itg1addlem3  25678  itg1climres  25694  itg2uba  25723  itg2splitlem  25728  elcpn  25914  dvexp  25933  dvexp2  25934  rolle  25970  cmvth  25971  mvth  25972  dvlip  25973  dvlipcn  25974  dvlip2  25975  dveq0  25980  dv11cn  25981  lhop1lem  25993  lhop2  25995  lhop  25996  dvcvx  26000  ftc2ditglem  26025  itgsubstlem  26028  ig1pval  26154  elply2  26174  coeid2  26217  coemul  26230  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem1  26381  mtest  26385  pserval2  26392  abelthlem1  26412  abelthlem3  26414  abelthlem8  26420  abelthlem9  26421  pige3ALT  26500  0cxp  26646  leibpi  26922  igamgam  27029  mule1  27128  bposlem5  27268  lgsval3  27295  lgsdinn0  27325  dchrvmasumlem1  27475  dchrisum0flblem1  27488  rpvmasum2  27492  padicval  27597  abssid  28250  abssnid  28252  axsegconlem1  29003  ax5seglem9  29023  axpasch  29027  axeuclidlem  29048  axcontlem2  29051  finsumvtxdg2ssteplem4  29635  usgr2wlkspthlem2  29844  crctcshlem4  29906  wwlknp  29929  wlkiswwlks2lem3  29957  wwlksnred  29978  wwlksnextproplem2  29996  usgrwwlks2on  30044  umgrwwlks2on  30045  clwlkclwwlklem2a  30086  clwwisshclwwsn  30104  clwwlknlbonbgr1  30127  clwwlkn1loopb  30131  clwwlkf  30135  clwwlkext2edg  30144  wwlksext2clwwlk  30145  erclwwlknsym  30158  erclwwlkntr  30159  clwwlknon1  30185  clwwlknonex2  30197  eupth2lem3lem3  30318  eucrct2eupth  30333  fusgreghash2wspv  30423  2clwwlk2clwwlklem  30434  2clwwlk2clwwlk  30438  numclwwlk1lem2f1  30445  grpoidinvlem4  30596  grpoinvval  30612  grpodivval  30624  ipval  30792  sspgval  30818  sspsval  30820  sspnval  30826  nmooval  30852  ipasslem1  30920  ipasslem4  30923  hial0  31191  hial02  31192  ocsh  31372  pjhval  31486  hosval  31829  homval  31830  hodval  31831  hfsval  31832  hfmval  31833  braval  32033  kbval  32043  eigvalval  32049  0hmop  32072  adj0  32083  lnopeq0i  32096  nmopcoi  32184  pjclem4  32288  pj3si  32296  hstoh  32321  strlem3a  32341  hstrlem3a  32349  mdexchi  32424  atcv0eq  32468  atcv1  32469  fpwrelmap  32824  cycpmco2lem4  33208  cycpmco2lem5  33209  fxpgaval  33246  smatfval  33958  measxun2  34373  measdivcst  34387  measdivcstALTV  34388  ddeval1  34397  ddeval0  34398  ballotlemfp1  34655  signswmnd  34720  signstfvneq0  34735  signstfvc  34737  ftc2re  34761  itgexpif  34769  bnj1128  35151  subfacp1lem3  35383  subfacp1lem5  35385  cvmlift2lem3  35506  msubco  35732  altopthsn  36162  ditgeq12d  36423  fnetr  36552  fnejoin2  36570  ttcsntrsucg  36723  bj-evalid  37407  finxpreclem3  37726  finxpreclem5  37728  finxpreclem6  37729  curf  37936  curunc  37940  matunitlindf  37956  poimirlem4  37962  poimirlem25  37983  mblfinlem2  37996  mblfinlem3  37997  mbfresfi  38004  itg2addnclem  38009  itg2addnc  38012  ftc1anclem5  38035  isbnd3  38122  bndss  38124  grposnOLD  38220  ghomco  38229  xrneq12  38740  lkrval  39551  pmapval  40220  polvalN  40368  watvalN  40456  ldilset  40572  ltrnset  40581  dilsetN  40616  trnsetN  40619  trlset  40624  trlval  40625  cdleme16b  40742  cdleme31fv1  40854  cdlemg1idlemN  41035  tgrpset  41208  tendoset  41222  erngset  41263  erngplus  41266  erngmul  41269  erngset-rN  41271  erngplus-rN  41274  dvaset  41468  dvaplusg  41472  dvamulr  41475  dvavadd  41478  dvavsca  41480  diafval  41494  dvhset  41544  dvhmulr  41549  dvhvadd  41555  dvhvsca  41564  docafvalN  41585  djafvalN  41597  dibfval  41604  dicfval  41638  dihfval  41694  dihval  41695  dihvalc  41696  dihvalb  41700  dochfval  41813  djhfval  41860  lcdval  42052  mapdfval  42090  mapdn0  42132  hvmapfval  42222  hdmap1fval  42259  hdmapfval  42290  hgmapfval  42349  fmpocos  42692  sn-it0e0  42865  zaddcomlem  42925  pw2f1ocnv  43486  hbtlem7  43574  relexp0a  44164  ntrclscls00  44514  dvconstbi  44782  expgrowth  44783  addrfv  44916  subrfv  44917  mulvfv  44918  refsum2cnlem1  45489  limcperiod  46079  cncfiooiccre  46344  dvbdfbdioolem1  46377  itgioocnicc  46426  fourierdlem73  46628  fourierdlem82  46637  fourierdlem94  46649  fourierdlem103  46658  fourierdlem104  46659  fourierdlem113  46668  sqwvfoura  46677  etransclem46  46729  nnfoctbdjlem  46904  ovn0  47015  smflim  47226  afveu  47616  afv2eu  47701  fvmptrabdm  47756  imasetpreimafvbijlemfo  47880  lighneallem3  48085  ppivalnnprm  48103  mogoldbblem  48211  fpprel2  48232  sbgoldbwt  48268  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbnd  48300  grimco  48380  cycl3grtri  48438  lmod0rng  48720  lmodvsmdi  48870  lincdifsn  48915  lcoel0  48919  islindeps2  48974  blenn0  49064  nn0sumshdiglemA  49110  itcoval0mpt  49157  rrx2plordisom  49214  nelsubclem  49557  aacllem  50291