Theorem sylan9eq 2791

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 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 2708

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

This theorem is referenced by:  sylan9req  2792  sylan9eqr  2793  difeq12  4073  uneq12  4115  ineq12  4167  ssdifim  4225  ifeq12  4498  ifbi  4502  ifeq12da  4513  preq12  4692  prprc  4724  opeq12  4831  eqsnuniex  5306  opthwiener  5462  opthhausdorff0  5466  xpeq12  5649  sosn  5711  nfimad  6028  coi2  6222  funprg  6546  funtpg  6547  funcnvtp  6555  funcnvqp  6556  funimass1  6574  fimadmfoALT  6757  f1orescnv  6789  resdif  6795  fvmpt2  6952  fvmptnf  6963  fveqressseq  7024  oveq12  7367  cbvmpov  7453  ovmpog  7517  fvmpopr2d  7520  caofinvl  7654  eqopi  7969  el2mpocsbcl  8027  fmpoco  8037  mposn  8045  fsuppeqg  8118  supp0cosupp0  8150  imacosupp  8151  mpocurryd  8211  fvmpocurryd  8213  rdgsucmptf  8359  frsucmpt  8369  oevn0  8442  oa0r  8465  om1r  8470  oe1m  8472  omass  8507  oeoalem  8524  oeoa  8525  oeoe  8527  qseq12  8699  map0g  8822  xpcomco  8995  sbthlem4  9018  sbthlem5  9019  xpmapenlem  9072  phplem2  9129  unxpdomlem3  9158  funsnfsupp  9295  ordtypelem7  9429  ttrcltr  9625  cardennn  9895  dfac9  10047  alephsing  10186  axcc3  10348  ac6num  10389  konigthlem  10479  canthp1lem2  10564  ordpipq  10853  ltrnq  10890  addclprlem2  10928  mulclprlem  10930  prlem934  10944  prlem936  10958  mulcmpblnrlem  10981  addcnsr  11046  mulcnsr  11047  axcnre  11075  recex  11769  rpnnen1lem3  12892  rpnnen1lem5  12894  xaddpnf1  13141  xaddpnf2  13142  xaddmnf1  13143  xaddmnf2  13144  rexadd  13147  xnn0xaddcl  13150  xaddnemnf  13151  xaddnepnf  13152  xadddilem  13209  addmodlteq  13869  om2uzrani  13875  om2uzrdg  13879  seqf1olem2  13965  seqf1o  13966  modexp  14161  faclbnd4lem3  14218  hashunsng  14315  hashwrdn  14470  lsw1  14490  swrdfv  14572  swrdccat  14658  ccats1pfxeqbi  14665  revfv  14686  cshwsublen  14719  wrdlen2  14867  wrdl2exs2  14869  wwlktovf1  14880  relexp0  14946  relexpcnv  14958  shftcan1  15006  remul2  15053  immul2  15060  sumss  15647  geomulcvg  15799  fprodss  15871  binomfallfaclem2  15963  bpolylem  15971  ef0lem  16001  efieq1re  16124  rpnnen2lem1  16139  ruclem3  16158  dvdsnegb  16200  dvdscmul  16209  dvds2ln  16216  dvds2add  16217  dvds2sub  16218  gcdn0val  16425  rpmulgcd  16484  lcmn0val  16522  odzval  16719  pcval  16772  pcmpt  16820  prmreclem4  16847  1arithlem2  16852  vdwlem8  16916  ramcl2lem  16937  ramtcl  16938  ramtub  16940  ramcl2  16944  ramcl  16957  setsval  17094  prfcl  18126  curf1cl  18151  curfcl  18155  hofcl  18182  yonedalem4c  18200  psssdm  18505  chneq12  18537  grplactval  18972  mulgnn0gsum  19010  cntzval  19250  f1omvdco2  19377  pmtrfinv  19390  psgnunilem5  19423  odlem2  19468  gexlem2  19511  lsmvalx  19568  efgtval  19652  efgredlema  19669  vrgpval  19696  cyggex  19827  gsumcom2  19904  fincygsubgodd  20043  dvdsrtr  20304  rnghmval  20376  abvtrivd  20765  lmhmco  20995  reslmhm  21004  lvecinv  21068  zrhmulg  21464  znzrhval  21501  ocvval  21622  mplmon2  22016  subrgasclcl  22022  coe1fv  22147  coe1fzgsumdlem  22247  evl1gsumdlem  22300  mat1dimscm  22419  dmatid  22439  scmatdmat  22459  mavmul0g  22497  1marepvmarrepid  22519  mdetunilem2  22557  gsummatr01lem3  22601  gsummatr01  22603  smadiadetlem3  22612  m2cpminvid2lem  22698  chpdmatlem2  22783  isopn3  23010  cnpval  23180  ptbasfi  23525  dfac14  23562  cnmptkk  23627  xkofvcn  23628  cnmptk1p  23629  cnmptk2  23630  xkocnv  23758  flfval  23934  ptcmplem3  23998  ptcmpg  24001  tmdmulg  24036  prdsxmslem2  24473  subgnm2  24578  nmoval  24659  fsum2cn  24818  pcovalg  24968  isclmp  25053  cphnm  25149  tcphnmval  25185  ovolctb  25447  ioorcl  25534  uniioombllem2  25540  itg1addlem3  25655  itg1climres  25671  itg2uba  25700  itg2splitlem  25705  elcpn  25892  dvexp  25913  dvexp2  25914  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvlipcn  25955  dvlip2  25956  dveq0  25961  dv11cn  25962  lhop1lem  25974  lhop2  25976  lhop  25977  dvcvx  25981  ftc2ditglem  26008  itgsubstlem  26011  ig1pval  26137  elply2  26157  coeid2  26200  coemul  26213  taylthlem2  26338  taylthlem2OLD  26339  ulmdvlem1  26365  mtest  26369  pserval2  26376  abelthlem1  26397  abelthlem3  26399  abelthlem8  26405  abelthlem9  26406  pige3ALT  26485  0cxp  26631  leibpi  26908  igamgam  27015  mule1  27114  bposlem5  27255  lgsval3  27282  lgsdinn0  27312  dchrvmasumlem1  27462  dchrisum0flblem1  27475  rpvmasum2  27479  padicval  27584  abssid  28237  abssnid  28239  axsegconlem1  28990  ax5seglem9  29010  axpasch  29014  axeuclidlem  29035  axcontlem2  29038  finsumvtxdg2ssteplem4  29622  usgr2wlkspthlem2  29831  crctcshlem4  29893  wwlknp  29916  wlkiswwlks2lem3  29944  wwlksnred  29965  wwlksnextproplem2  29983  usgrwwlks2on  30031  umgrwwlks2on  30032  clwlkclwwlklem2a  30073  clwwisshclwwsn  30091  clwwlknlbonbgr1  30114  clwwlkn1loopb  30118  clwwlkf  30122  clwwlkext2edg  30131  wwlksext2clwwlk  30132  erclwwlknsym  30145  erclwwlkntr  30146  clwwlknon1  30172  clwwlknonex2  30184  eupth2lem3lem3  30305  eucrct2eupth  30320  fusgreghash2wspv  30410  2clwwlk2clwwlklem  30421  2clwwlk2clwwlk  30425  numclwwlk1lem2f1  30432  grpoidinvlem4  30582  grpoinvval  30598  grpodivval  30610  ipval  30778  sspgval  30804  sspsval  30806  sspnval  30812  nmooval  30838  ipasslem1  30906  ipasslem4  30909  hial0  31177  hial02  31178  ocsh  31358  pjhval  31472  hosval  31815  homval  31816  hodval  31817  hfsval  31818  hfmval  31819  braval  32019  kbval  32029  eigvalval  32035  0hmop  32058  adj0  32069  lnopeq0i  32082  nmopcoi  32170  pjclem4  32274  pj3si  32282  hstoh  32307  strlem3a  32327  hstrlem3a  32335  mdexchi  32410  atcv0eq  32454  atcv1  32455  fpwrelmap  32812  cycpmco2lem4  33211  cycpmco2lem5  33212  fxpgaval  33249  smatfval  33952  measxun2  34367  measdivcst  34381  measdivcstALTV  34382  ddeval1  34391  ddeval0  34392  ballotlemfp1  34649  signswmnd  34714  signstfvneq0  34729  signstfvc  34731  ftc2re  34755  itgexpif  34763  bnj1128  35146  subfacp1lem3  35376  subfacp1lem5  35378  cvmlift2lem3  35499  msubco  35725  altopthsn  36155  ditgeq12d  36416  fnetr  36545  fnejoin2  36563  bj-evalid  37281  finxpreclem3  37598  finxpreclem5  37600  finxpreclem6  37601  curf  37799  curunc  37803  matunitlindf  37819  poimirlem4  37825  poimirlem25  37846  mblfinlem2  37859  mblfinlem3  37860  mbfresfi  37867  itg2addnclem  37872  itg2addnc  37875  ftc1anclem5  37898  isbnd3  37985  bndss  37987  grposnOLD  38083  ghomco  38092  xrneq12  38587  lkrval  39348  pmapval  40017  polvalN  40165  watvalN  40253  ldilset  40369  ltrnset  40378  dilsetN  40413  trnsetN  40416  trlset  40421  trlval  40422  cdleme16b  40539  cdleme31fv1  40651  cdlemg1idlemN  40832  tgrpset  41005  tendoset  41019  erngset  41060  erngplus  41063  erngmul  41066  erngset-rN  41068  erngplus-rN  41071  dvaset  41265  dvaplusg  41269  dvamulr  41272  dvavadd  41275  dvavsca  41277  diafval  41291  dvhset  41341  dvhmulr  41346  dvhvadd  41352  dvhvsca  41361  docafvalN  41382  djafvalN  41394  dibfval  41401  dicfval  41435  dihfval  41491  dihval  41492  dihvalc  41493  dihvalb  41497  dochfval  41610  djhfval  41657  lcdval  41849  mapdfval  41887  mapdn0  41929  hvmapfval  42019  hdmap1fval  42056  hdmapfval  42087  hgmapfval  42146  fmpocos  42490  sn-it0e0  42671  zaddcomlem  42718  pw2f1ocnv  43279  hbtlem7  43367  relexp0a  43957  ntrclscls00  44307  dvconstbi  44575  expgrowth  44576  addrfv  44709  subrfv  44710  mulvfv  44711  refsum2cnlem1  45282  limcperiod  45874  cncfiooiccre  46139  dvbdfbdioolem1  46172  itgioocnicc  46221  fourierdlem73  46423  fourierdlem82  46432  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem113  46463  sqwvfoura  46472  etransclem46  46524  nnfoctbdjlem  46699  ovn0  46810  smflim  47021  afveu  47399  afv2eu  47484  fvmptrabdm  47539  imasetpreimafvbijlemfo  47651  lighneallem3  47853  mogoldbblem  47966  fpprel2  47987  sbgoldbwt  48023  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  bgoldbtbnd  48055  grimco  48135  cycl3grtri  48193  lmod0rng  48475  lmodvsmdi  48625  lincdifsn  48670  lcoel0  48674  islindeps2  48729  blenn0  48819  nn0sumshdiglemA  48865  itcoval0mpt  48912  rrx2plordisom  48969  nelsubclem  49312  aacllem  50046