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  4075  uneq12  4117  ineq12  4169  ssdifim  4227  ifeq12  4500  ifbi  4504  ifeq12da  4515  preq12  4694  prprc  4726  opeq12  4833  eqsnuniex  5308  opthwiener  5470  opthhausdorff0  5474  xpeq12  5657  sosn  5719  nfimad  6036  coi2  6230  funprg  6554  funtpg  6555  funcnvtp  6563  funcnvqp  6564  funimass1  6582  fimadmfoALT  6765  f1orescnv  6797  resdif  6803  fvmpt2  6961  fvmptnf  6972  fveqressseq  7033  oveq12  7377  cbvmpov  7463  ovmpog  7527  fvmpopr2d  7530  caofinvl  7664  eqopi  7979  el2mpocsbcl  8037  fmpoco  8047  mposn  8055  fsuppeqg  8128  supp0cosupp0  8160  imacosupp  8161  mpocurryd  8221  fvmpocurryd  8223  rdgsucmptf  8369  frsucmpt  8379  oevn0  8452  oa0r  8475  om1r  8480  oe1m  8482  omass  8517  oeoalem  8534  oeoa  8535  oeoe  8537  qseq12  8710  map0g  8834  xpcomco  9007  sbthlem4  9030  sbthlem5  9031  xpmapenlem  9084  phplem2  9141  unxpdomlem3  9170  funsnfsupp  9307  ordtypelem7  9441  ttrcltr  9637  cardennn  9907  dfac9  10059  alephsing  10198  axcc3  10360  ac6num  10401  konigthlem  10491  canthp1lem2  10576  ordpipq  10865  ltrnq  10902  addclprlem2  10940  mulclprlem  10942  prlem934  10956  prlem936  10970  mulcmpblnrlem  10993  addcnsr  11058  mulcnsr  11059  axcnre  11087  recex  11781  rpnnen1lem3  12904  rpnnen1lem5  12906  xaddpnf1  13153  xaddpnf2  13154  xaddmnf1  13155  xaddmnf2  13156  rexadd  13159  xnn0xaddcl  13162  xaddnemnf  13163  xaddnepnf  13164  xadddilem  13221  addmodlteq  13881  om2uzrani  13887  om2uzrdg  13891  seqf1olem2  13977  seqf1o  13978  modexp  14173  faclbnd4lem3  14230  hashunsng  14327  hashwrdn  14482  lsw1  14502  swrdfv  14584  swrdccat  14670  ccats1pfxeqbi  14677  revfv  14698  cshwsublen  14731  wrdlen2  14879  wrdl2exs2  14881  wwlktovf1  14892  relexp0  14958  relexpcnv  14970  shftcan1  15018  remul2  15065  immul2  15072  sumss  15659  geomulcvg  15811  fprodss  15883  binomfallfaclem2  15975  bpolylem  15983  ef0lem  16013  efieq1re  16136  rpnnen2lem1  16151  ruclem3  16170  dvdsnegb  16212  dvdscmul  16221  dvds2ln  16228  dvds2add  16229  dvds2sub  16230  gcdn0val  16437  rpmulgcd  16496  lcmn0val  16534  odzval  16731  pcval  16784  pcmpt  16832  prmreclem4  16859  1arithlem2  16864  vdwlem8  16928  ramcl2lem  16949  ramtcl  16950  ramtub  16952  ramcl2  16956  ramcl  16969  setsval  17106  prfcl  18138  curf1cl  18163  curfcl  18167  hofcl  18194  yonedalem4c  18212  psssdm  18517  chneq12  18549  grplactval  18984  mulgnn0gsum  19022  cntzval  19262  f1omvdco2  19389  pmtrfinv  19402  psgnunilem5  19435  odlem2  19480  gexlem2  19523  lsmvalx  19580  efgtval  19664  efgredlema  19681  vrgpval  19708  cyggex  19839  gsumcom2  19916  fincygsubgodd  20055  dvdsrtr  20316  rnghmval  20388  abvtrivd  20777  lmhmco  21007  reslmhm  21016  lvecinv  21080  zrhmulg  21476  znzrhval  21513  ocvval  21634  mplmon2  22028  subrgasclcl  22034  coe1fv  22159  coe1fzgsumdlem  22259  evl1gsumdlem  22312  mat1dimscm  22431  dmatid  22451  scmatdmat  22471  mavmul0g  22509  1marepvmarrepid  22531  mdetunilem2  22569  gsummatr01lem3  22613  gsummatr01  22615  smadiadetlem3  22624  m2cpminvid2lem  22710  chpdmatlem2  22795  isopn3  23022  cnpval  23192  ptbasfi  23537  dfac14  23574  cnmptkk  23639  xkofvcn  23640  cnmptk1p  23641  cnmptk2  23642  xkocnv  23770  flfval  23946  ptcmplem3  24010  ptcmpg  24013  tmdmulg  24048  prdsxmslem2  24485  subgnm2  24590  nmoval  24671  fsum2cn  24830  pcovalg  24980  isclmp  25065  cphnm  25161  tcphnmval  25197  ovolctb  25459  ioorcl  25546  uniioombllem2  25552  itg1addlem3  25667  itg1climres  25683  itg2uba  25712  itg2splitlem  25717  elcpn  25904  dvexp  25925  dvexp2  25926  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvlipcn  25967  dvlip2  25968  dveq0  25973  dv11cn  25974  lhop1lem  25986  lhop2  25988  lhop  25989  dvcvx  25993  ftc2ditglem  26020  itgsubstlem  26023  ig1pval  26149  elply2  26169  coeid2  26212  coemul  26225  taylthlem2  26350  taylthlem2OLD  26351  ulmdvlem1  26377  mtest  26381  pserval2  26388  abelthlem1  26409  abelthlem3  26411  abelthlem8  26417  abelthlem9  26418  pige3ALT  26497  0cxp  26643  leibpi  26920  igamgam  27027  mule1  27126  bposlem5  27267  lgsval3  27294  lgsdinn0  27324  dchrvmasumlem1  27474  dchrisum0flblem1  27487  rpvmasum2  27491  padicval  27596  abssid  28249  abssnid  28251  axsegconlem1  29002  ax5seglem9  29022  axpasch  29026  axeuclidlem  29047  axcontlem2  29050  finsumvtxdg2ssteplem4  29634  usgr2wlkspthlem2  29843  crctcshlem4  29905  wwlknp  29928  wlkiswwlks2lem3  29956  wwlksnred  29977  wwlksnextproplem2  29995  usgrwwlks2on  30043  umgrwwlks2on  30044  clwlkclwwlklem2a  30085  clwwisshclwwsn  30103  clwwlknlbonbgr1  30126  clwwlkn1loopb  30130  clwwlkf  30134  clwwlkext2edg  30143  wwlksext2clwwlk  30144  erclwwlknsym  30157  erclwwlkntr  30158  clwwlknon1  30184  clwwlknonex2  30196  eupth2lem3lem3  30317  eucrct2eupth  30332  fusgreghash2wspv  30422  2clwwlk2clwwlklem  30433  2clwwlk2clwwlk  30437  numclwwlk1lem2f1  30444  grpoidinvlem4  30595  grpoinvval  30611  grpodivval  30623  ipval  30791  sspgval  30817  sspsval  30819  sspnval  30825  nmooval  30851  ipasslem1  30919  ipasslem4  30922  hial0  31190  hial02  31191  ocsh  31371  pjhval  31485  hosval  31828  homval  31829  hodval  31830  hfsval  31831  hfmval  31832  braval  32032  kbval  32042  eigvalval  32048  0hmop  32071  adj0  32082  lnopeq0i  32095  nmopcoi  32183  pjclem4  32287  pj3si  32295  hstoh  32320  strlem3a  32340  hstrlem3a  32348  mdexchi  32423  atcv0eq  32467  atcv1  32468  fpwrelmap  32823  cycpmco2lem4  33223  cycpmco2lem5  33224  fxpgaval  33261  smatfval  33973  measxun2  34388  measdivcst  34402  measdivcstALTV  34403  ddeval1  34412  ddeval0  34413  ballotlemfp1  34670  signswmnd  34735  signstfvneq0  34750  signstfvc  34752  ftc2re  34776  itgexpif  34784  bnj1128  35166  subfacp1lem3  35398  subfacp1lem5  35400  cvmlift2lem3  35521  msubco  35747  altopthsn  36177  ditgeq12d  36438  fnetr  36567  fnejoin2  36585  bj-evalid  37329  finxpreclem3  37648  finxpreclem5  37650  finxpreclem6  37651  curf  37849  curunc  37853  matunitlindf  37869  poimirlem4  37875  poimirlem25  37896  mblfinlem2  37909  mblfinlem3  37910  mbfresfi  37917  itg2addnclem  37922  itg2addnc  37925  ftc1anclem5  37948  isbnd3  38035  bndss  38037  grposnOLD  38133  ghomco  38142  xrneq12  38653  lkrval  39464  pmapval  40133  polvalN  40281  watvalN  40369  ldilset  40485  ltrnset  40494  dilsetN  40529  trnsetN  40532  trlset  40537  trlval  40538  cdleme16b  40655  cdleme31fv1  40767  cdlemg1idlemN  40948  tgrpset  41121  tendoset  41135  erngset  41176  erngplus  41179  erngmul  41182  erngset-rN  41184  erngplus-rN  41187  dvaset  41381  dvaplusg  41385  dvamulr  41388  dvavadd  41391  dvavsca  41393  diafval  41407  dvhset  41457  dvhmulr  41462  dvhvadd  41468  dvhvsca  41477  docafvalN  41498  djafvalN  41510  dibfval  41517  dicfval  41551  dihfval  41607  dihval  41608  dihvalc  41609  dihvalb  41613  dochfval  41726  djhfval  41773  lcdval  41965  mapdfval  42003  mapdn0  42045  hvmapfval  42135  hdmap1fval  42172  hdmapfval  42203  hgmapfval  42262  fmpocos  42606  sn-it0e0  42786  zaddcomlem  42833  pw2f1ocnv  43394  hbtlem7  43482  relexp0a  44072  ntrclscls00  44422  dvconstbi  44690  expgrowth  44691  addrfv  44824  subrfv  44825  mulvfv  44826  refsum2cnlem1  45397  limcperiod  45988  cncfiooiccre  46253  dvbdfbdioolem1  46286  itgioocnicc  46335  fourierdlem73  46537  fourierdlem82  46546  fourierdlem94  46558  fourierdlem103  46567  fourierdlem104  46568  fourierdlem113  46577  sqwvfoura  46586  etransclem46  46638  nnfoctbdjlem  46813  ovn0  46924  smflim  47135  afveu  47513  afv2eu  47598  fvmptrabdm  47653  imasetpreimafvbijlemfo  47765  lighneallem3  47967  mogoldbblem  48080  fpprel2  48101  sbgoldbwt  48137  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  bgoldbtbnd  48169  grimco  48249  cycl3grtri  48307  lmod0rng  48589  lmodvsmdi  48739  lincdifsn  48784  lcoel0  48788  islindeps2  48843  blenn0  48933  nn0sumshdiglemA  48979  itcoval0mpt  49026  rrx2plordisom  49083  nelsubclem  49426  aacllem  50160