Theorem sylan9eq 2793

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  sylan9req  2794  sylan9eqr  2795  difeq12  4118  uneq12  4159  ineq12  4208  ssdifim  4263  ifeq12  4547  ifbi  4551  ifeq12da  4562  preq12  4740  prprc  4772  opeq12  4876  eqsnuniex  5360  opthwiener  5515  opthhausdorff0  5519  xpeq12  5702  sosn  5763  nfimad  6069  coi2  6263  funprg  6603  funtpg  6604  funcnvtp  6612  funcnvqp  6613  funimass1  6631  fimadmfoALT  6817  f1orescnv  6849  resdif  6855  fvmpt2  7010  fvmptnf  7021  fveqressseq  7082  oveq12  7418  cbvmpov  7504  ovmpog  7567  fvmpopr2d  7569  caofinvl  7700  eqopi  8011  el2mpocsbcl  8071  fmpoco  8081  mposn  8089  fsuppeqg  8161  supp0cosupp0  8193  imacosupp  8194  mpocurryd  8254  fvmpocurryd  8256  wrecseq123OLD  8300  rdgsucmptf  8428  frsucmpt  8438  oevn0  8515  oa0r  8538  om1r  8543  oe1m  8545  omass  8580  oeoalem  8596  oeoa  8597  oeoe  8599  qseq12  8761  map0g  8878  xpcomco  9062  sbthlem4  9086  sbthlem5  9087  xpmapenlem  9144  phplem2  9208  phplem3OLD  9219  phplem4OLD  9220  unxpdomlem3  9252  funsnfsupp  9387  ordtypelem7  9519  ttrcltr  9711  cardennn  9978  dfac9  10131  alephsing  10271  axcc3  10433  ac6num  10474  konigthlem  10563  canthp1lem2  10648  ordpipq  10937  ltrnq  10974  addclprlem2  11012  mulclprlem  11014  prlem934  11028  prlem936  11042  mulcmpblnrlem  11065  addcnsr  11130  mulcnsr  11131  axcnre  11159  recex  11846  rpnnen1lem3  12963  rpnnen1lem5  12965  xaddpnf1  13205  xaddpnf2  13206  xaddmnf1  13207  xaddmnf2  13208  rexadd  13211  xnn0xaddcl  13214  xaddnemnf  13215  xaddnepnf  13216  xadddilem  13273  addmodlteq  13911  om2uzrani  13917  om2uzrdg  13921  seqf1olem2  14008  seqf1o  14009  modexp  14201  faclbnd4lem3  14255  hashunsng  14352  hashwrdn  14497  lsw1  14517  swrdfv  14598  swrdccat  14685  ccats1pfxeqbi  14692  revfv  14713  cshwsublen  14746  wrdlen2  14895  wrdl2exs2  14897  wwlktovf1  14908  relexp0  14970  relexpcnv  14982  shftcan1  15030  remul2  15077  immul2  15084  sumss  15670  geomulcvg  15822  fprodss  15892  binomfallfaclem2  15984  bpolylem  15992  ef0lem  16022  efieq1re  16142  rpnnen2lem1  16157  ruclem3  16176  dvdsnegb  16217  dvdscmul  16226  dvds2ln  16232  dvds2add  16233  dvds2sub  16234  gcdn0val  16439  rpmulgcd  16498  lcmn0val  16532  odzval  16724  pcval  16777  pcmpt  16825  prmreclem4  16852  1arithlem2  16857  vdwlem8  16921  ramcl2lem  16942  ramtcl  16943  ramtub  16945  ramcl2  16949  ramcl  16962  setsval  17100  prfcl  18155  curf1cl  18181  curfcl  18185  hofcl  18212  yonedalem4c  18230  psssdm  18535  grplactval  18925  mulgnn0gsum  18960  cntzval  19185  f1omvdco2  19316  pmtrfinv  19329  psgnunilem5  19362  odlem2  19407  gexlem2  19450  lsmvalx  19507  efgtval  19591  efgredlema  19608  vrgpval  19635  cyggex  19766  gsumcom2  19843  fincygsubgodd  19982  dvdsrtr  20182  abvtrivd  20448  lmhmco  20654  reslmhm  20663  lvecinv  20726  zrhmulg  21059  znzrhval  21102  ocvval  21220  mplmon2  21622  subrgasclcl  21628  coe1fv  21730  coe1fzgsumdlem  21825  evl1gsumdlem  21875  mat1dimscm  21977  dmatid  21997  scmatdmat  22017  mavmul0g  22055  1marepvmarrepid  22077  mdetunilem2  22115  gsummatr01lem3  22159  gsummatr01  22161  smadiadetlem3  22170  m2cpminvid2lem  22256  chpdmatlem2  22341  isopn3  22570  cnpval  22740  ptbasfi  23085  dfac14  23122  cnmptkk  23187  xkofvcn  23188  cnmptk1p  23189  cnmptk2  23190  xkocnv  23318  flfval  23494  ptcmplem3  23558  ptcmpg  23561  tmdmulg  23596  prdsxmslem2  24038  subgnm2  24143  nmoval  24232  fsum2cn  24387  pcovalg  24528  isclmp  24613  cphnm  24710  tcphnmval  24746  ovolctb  25007  ioorcl  25094  uniioombllem2  25100  itg1addlem3  25215  itg1climres  25232  itg2uba  25261  itg2splitlem  25266  elcpn  25451  dvexp  25470  dvexp2  25471  rolle  25507  cmvth  25508  mvth  25509  dvlip  25510  dvlipcn  25511  dvlip2  25512  dveq0  25517  dv11cn  25518  lhop1lem  25530  lhop2  25532  lhop  25533  dvcvx  25537  ftc2ditglem  25562  itgsubstlem  25565  ig1pval  25690  elply2  25710  coeid2  25753  coemul  25766  taylthlem2  25886  ulmdvlem1  25912  mtest  25916  pserval2  25923  abelthlem1  25943  abelthlem3  25945  abelthlem8  25951  abelthlem9  25952  pige3ALT  26029  0cxp  26174  leibpi  26447  igamgam  26553  mule1  26652  bposlem5  26791  lgsval3  26818  lgsdinn0  26848  dchrvmasumlem1  26998  dchrisum0flblem1  27011  rpvmasum2  27015  padicval  27120  axsegconlem1  28175  ax5seglem9  28195  axpasch  28199  axeuclidlem  28220  axcontlem2  28223  finsumvtxdg2ssteplem4  28805  usgr2wlkspthlem2  29015  crctcshlem4  29074  wwlknp  29097  wlkiswwlks2lem3  29125  wwlksnred  29146  wwlksnextproplem2  29164  umgrwwlks2on  29211  clwlkclwwlklem2a  29251  clwwisshclwwsn  29269  clwwlknlbonbgr1  29292  clwwlkn1loopb  29296  clwwlkf  29300  clwwlkext2edg  29309  wwlksext2clwwlk  29310  erclwwlknsym  29323  erclwwlkntr  29324  clwwlknon1  29350  clwwlknonex2  29362  eupth2lem3lem3  29483  eucrct2eupth  29498  fusgreghash2wspv  29588  2clwwlk2clwwlklem  29599  2clwwlk2clwwlk  29603  numclwwlk1lem2f1  29610  grpoidinvlem4  29760  grpoinvval  29776  grpodivval  29788  ipval  29956  sspgval  29982  sspsval  29984  sspnval  29990  nmooval  30016  ipasslem1  30084  ipasslem4  30087  hial0  30355  hial02  30356  ocsh  30536  pjhval  30650  hosval  30993  homval  30994  hodval  30995  hfsval  30996  hfmval  30997  braval  31197  kbval  31207  eigvalval  31213  0hmop  31236  adj0  31247  lnopeq0i  31260  nmopcoi  31348  pjclem4  31452  pj3si  31460  hstoh  31485  strlem3a  31505  hstrlem3a  31513  mdexchi  31588  atcv0eq  31632  atcv1  31633  fpwrelmap  31958  cycpmco2lem4  32288  cycpmco2lem5  32289  smatfval  32775  measxun2  33208  measdivcst  33222  measdivcstALTV  33223  ddeval1  33232  ddeval0  33233  ballotlemfp1  33490  signswmnd  33568  signstfvneq0  33583  signstfvc  33585  ftc2re  33610  itgexpif  33618  bnj1128  34001  subfacp1lem3  34173  subfacp1lem5  34175  cvmlift2lem3  34296  msubco  34522  altopthsn  34933  gg-cmvth  35181  fnetr  35236  fnejoin2  35254  bj-evalid  35957  finxpreclem3  36274  finxpreclem5  36276  finxpreclem6  36277  curf  36466  curunc  36470  matunitlindf  36486  poimirlem4  36492  poimirlem25  36513  mblfinlem2  36526  mblfinlem3  36527  mbfresfi  36534  itg2addnclem  36539  itg2addnc  36542  ftc1anclem5  36565  isbnd3  36652  bndss  36654  grposnOLD  36750  ghomco  36759  xrneq12  37253  lkrval  37958  pmapval  38628  polvalN  38776  watvalN  38864  ldilset  38980  ltrnset  38989  dilsetN  39024  trnsetN  39027  trlset  39032  trlval  39033  cdleme16b  39150  cdleme31fv1  39262  cdlemg1idlemN  39443  tgrpset  39616  tendoset  39630  erngset  39671  erngplus  39674  erngmul  39677  erngset-rN  39679  erngplus-rN  39682  dvaset  39876  dvaplusg  39880  dvamulr  39883  dvavadd  39886  dvavsca  39888  diafval  39902  dvhset  39952  dvhmulr  39957  dvhvadd  39963  dvhvsca  39972  docafvalN  39993  djafvalN  40005  dibfval  40012  dicfval  40046  dihfval  40102  dihval  40103  dihvalc  40104  dihvalb  40108  dochfval  40221  djhfval  40268  lcdval  40460  mapdfval  40498  mapdn0  40540  hvmapfval  40630  hdmap1fval  40667  hdmapfval  40698  hgmapfval  40757  fmpocos  41056  sn-it0e0  41288  zaddcomlem  41324  pw2f1ocnv  41776  hbtlem7  41867  relexp0a  42467  ntrclscls00  42817  dvconstbi  43093  expgrowth  43094  addrfv  43228  subrfv  43229  mulvfv  43230  refsum2cnlem1  43721  limcperiod  44344  cncfiooiccre  44611  dvbdfbdioolem1  44644  itgioocnicc  44693  fourierdlem73  44895  fourierdlem82  44904  fourierdlem94  44916  fourierdlem103  44925  fourierdlem104  44926  fourierdlem113  44935  sqwvfoura  44944  etransclem46  44996  nnfoctbdjlem  45171  ovn0  45282  smflim  45493  afveu  45861  afv2eu  45946  fvmptrabdm  46001  imasetpreimafvbijlemfo  46073  lighneallem3  46275  mogoldbblem  46388  fpprel2  46409  sbgoldbwt  46445  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbnd  46477  lmod0rng  46642  rnghmval  46689  lmodvsmdi  47058  lincdifsn  47105  lcoel0  47109  islindeps2  47164  blenn0  47259  nn0sumshdiglemA  47305  itcoval0mpt  47352  rrx2plordisom  47409  aacllem  47848