Theorem sylan9eq 2797

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  sylan9req  2798  sylan9eqr  2799  difeq12  4121  uneq12  4163  ineq12  4215  ssdifim  4273  ifeq12  4544  ifbi  4548  ifeq12da  4559  preq12  4735  prprc  4767  opeq12  4875  eqsnuniex  5361  opthwiener  5519  opthhausdorff0  5523  xpeq12  5710  sosn  5772  nfimad  6087  coi2  6283  funprg  6620  funtpg  6621  funcnvtp  6629  funcnvqp  6630  funimass1  6648  fimadmfoALT  6831  f1orescnv  6863  resdif  6869  fvmpt2  7027  fvmptnf  7038  fveqressseq  7099  oveq12  7440  cbvmpov  7528  ovmpog  7592  fvmpopr2d  7595  caofinvl  7729  eqopi  8050  el2mpocsbcl  8110  fmpoco  8120  mposn  8128  fsuppeqg  8201  supp0cosupp0  8233  imacosupp  8234  mpocurryd  8294  fvmpocurryd  8296  wrecseq123OLD  8340  rdgsucmptf  8468  frsucmpt  8478  oevn0  8553  oa0r  8576  om1r  8581  oe1m  8583  omass  8618  oeoalem  8634  oeoa  8635  oeoe  8637  qseq12  8806  map0g  8924  xpcomco  9102  sbthlem4  9126  sbthlem5  9127  xpmapenlem  9184  phplem2  9245  phplem3OLD  9256  phplem4OLD  9257  unxpdomlem3  9288  funsnfsupp  9432  ordtypelem7  9564  ttrcltr  9756  cardennn  10023  dfac9  10177  alephsing  10316  axcc3  10478  ac6num  10519  konigthlem  10608  canthp1lem2  10693  ordpipq  10982  ltrnq  11019  addclprlem2  11057  mulclprlem  11059  prlem934  11073  prlem936  11087  mulcmpblnrlem  11110  addcnsr  11175  mulcnsr  11176  axcnre  11204  recex  11895  rpnnen1lem3  13021  rpnnen1lem5  13023  xaddpnf1  13268  xaddpnf2  13269  xaddmnf1  13270  xaddmnf2  13271  rexadd  13274  xnn0xaddcl  13277  xaddnemnf  13278  xaddnepnf  13279  xadddilem  13336  addmodlteq  13987  om2uzrani  13993  om2uzrdg  13997  seqf1olem2  14083  seqf1o  14084  modexp  14277  faclbnd4lem3  14334  hashunsng  14431  hashwrdn  14585  lsw1  14605  swrdfv  14686  swrdccat  14773  ccats1pfxeqbi  14780  revfv  14801  cshwsublen  14834  wrdlen2  14983  wrdl2exs2  14985  wwlktovf1  14996  relexp0  15062  relexpcnv  15074  shftcan1  15122  remul2  15169  immul2  15176  sumss  15760  geomulcvg  15912  fprodss  15984  binomfallfaclem2  16076  bpolylem  16084  ef0lem  16114  efieq1re  16235  rpnnen2lem1  16250  ruclem3  16269  dvdsnegb  16311  dvdscmul  16320  dvds2ln  16326  dvds2add  16327  dvds2sub  16328  gcdn0val  16535  rpmulgcd  16594  lcmn0val  16632  odzval  16829  pcval  16882  pcmpt  16930  prmreclem4  16957  1arithlem2  16962  vdwlem8  17026  ramcl2lem  17047  ramtcl  17048  ramtub  17050  ramcl2  17054  ramcl  17067  setsval  17204  prfcl  18248  curf1cl  18273  curfcl  18277  hofcl  18304  yonedalem4c  18322  psssdm  18627  grplactval  19060  mulgnn0gsum  19098  cntzval  19339  f1omvdco2  19466  pmtrfinv  19479  psgnunilem5  19512  odlem2  19557  gexlem2  19600  lsmvalx  19657  efgtval  19741  efgredlema  19758  vrgpval  19785  cyggex  19916  gsumcom2  19993  fincygsubgodd  20132  dvdsrtr  20368  rnghmval  20440  abvtrivd  20833  lmhmco  21042  reslmhm  21051  lvecinv  21115  zrhmulg  21520  znzrhval  21565  ocvval  21685  mplmon2  22085  subrgasclcl  22091  coe1fv  22208  coe1fzgsumdlem  22307  evl1gsumdlem  22360  mat1dimscm  22481  dmatid  22501  scmatdmat  22521  mavmul0g  22559  1marepvmarrepid  22581  mdetunilem2  22619  gsummatr01lem3  22663  gsummatr01  22665  smadiadetlem3  22674  m2cpminvid2lem  22760  chpdmatlem2  22845  isopn3  23074  cnpval  23244  ptbasfi  23589  dfac14  23626  cnmptkk  23691  xkofvcn  23692  cnmptk1p  23693  cnmptk2  23694  xkocnv  23822  flfval  23998  ptcmplem3  24062  ptcmpg  24065  tmdmulg  24100  prdsxmslem2  24542  subgnm2  24647  nmoval  24736  fsum2cn  24895  pcovalg  25045  isclmp  25130  cphnm  25227  tcphnmval  25263  ovolctb  25525  ioorcl  25612  uniioombllem2  25618  itg1addlem3  25733  itg1climres  25749  itg2uba  25778  itg2splitlem  25783  elcpn  25970  dvexp  25991  dvexp2  25992  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlipcn  26033  dvlip2  26034  dveq0  26039  dv11cn  26040  lhop1lem  26052  lhop2  26054  lhop  26055  dvcvx  26059  ftc2ditglem  26086  itgsubstlem  26089  ig1pval  26215  elply2  26235  coeid2  26278  coemul  26291  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem1  26443  mtest  26447  pserval2  26454  abelthlem1  26475  abelthlem3  26477  abelthlem8  26483  abelthlem9  26484  pige3ALT  26562  0cxp  26708  leibpi  26985  igamgam  27092  mule1  27191  bposlem5  27332  lgsval3  27359  lgsdinn0  27389  dchrvmasumlem1  27539  dchrisum0flblem1  27552  rpvmasum2  27556  padicval  27661  abssid  28265  abssnid  28267  cutpw2  28417  axsegconlem1  28932  ax5seglem9  28952  axpasch  28956  axeuclidlem  28977  axcontlem2  28980  finsumvtxdg2ssteplem4  29566  usgr2wlkspthlem2  29778  crctcshlem4  29840  wwlknp  29863  wlkiswwlks2lem3  29891  wwlksnred  29912  wwlksnextproplem2  29930  umgrwwlks2on  29977  clwlkclwwlklem2a  30017  clwwisshclwwsn  30035  clwwlknlbonbgr1  30058  clwwlkn1loopb  30062  clwwlkf  30066  clwwlkext2edg  30075  wwlksext2clwwlk  30076  erclwwlknsym  30089  erclwwlkntr  30090  clwwlknon1  30116  clwwlknonex2  30128  eupth2lem3lem3  30249  eucrct2eupth  30264  fusgreghash2wspv  30354  2clwwlk2clwwlklem  30365  2clwwlk2clwwlk  30369  numclwwlk1lem2f1  30376  grpoidinvlem4  30526  grpoinvval  30542  grpodivval  30554  ipval  30722  sspgval  30748  sspsval  30750  sspnval  30756  nmooval  30782  ipasslem1  30850  ipasslem4  30853  hial0  31121  hial02  31122  ocsh  31302  pjhval  31416  hosval  31759  homval  31760  hodval  31761  hfsval  31762  hfmval  31763  braval  31963  kbval  31973  eigvalval  31979  0hmop  32002  adj0  32013  lnopeq0i  32026  nmopcoi  32114  pjclem4  32218  pj3si  32226  hstoh  32251  strlem3a  32271  hstrlem3a  32279  mdexchi  32354  atcv0eq  32398  atcv1  32399  fpwrelmap  32744  cycpmco2lem4  33149  cycpmco2lem5  33150  smatfval  33794  measxun2  34211  measdivcst  34225  measdivcstALTV  34226  ddeval1  34235  ddeval0  34236  ballotlemfp1  34494  signswmnd  34572  signstfvneq0  34587  signstfvc  34589  ftc2re  34613  itgexpif  34621  bnj1128  35004  subfacp1lem3  35187  subfacp1lem5  35189  cvmlift2lem3  35310  msubco  35536  altopthsn  35962  ditgeq12d  36223  fnetr  36352  fnejoin2  36370  bj-evalid  37077  finxpreclem3  37394  finxpreclem5  37396  finxpreclem6  37397  curf  37605  curunc  37609  matunitlindf  37625  poimirlem4  37631  poimirlem25  37652  mblfinlem2  37665  mblfinlem3  37666  mbfresfi  37673  itg2addnclem  37678  itg2addnc  37681  ftc1anclem5  37704  isbnd3  37791  bndss  37793  grposnOLD  37889  ghomco  37898  xrneq12  38384  lkrval  39089  pmapval  39759  polvalN  39907  watvalN  39995  ldilset  40111  ltrnset  40120  dilsetN  40155  trnsetN  40158  trlset  40163  trlval  40164  cdleme16b  40281  cdleme31fv1  40393  cdlemg1idlemN  40574  tgrpset  40747  tendoset  40761  erngset  40802  erngplus  40805  erngmul  40808  erngset-rN  40810  erngplus-rN  40813  dvaset  41007  dvaplusg  41011  dvamulr  41014  dvavadd  41017  dvavsca  41019  diafval  41033  dvhset  41083  dvhmulr  41088  dvhvadd  41094  dvhvsca  41103  docafvalN  41124  djafvalN  41136  dibfval  41143  dicfval  41177  dihfval  41233  dihval  41234  dihvalc  41235  dihvalb  41239  dochfval  41352  djhfval  41399  lcdval  41591  mapdfval  41629  mapdn0  41671  hvmapfval  41761  hdmap1fval  41798  hdmapfval  41829  hgmapfval  41888  fmpocos  42275  sn-it0e0  42445  zaddcomlem  42481  pw2f1ocnv  43049  hbtlem7  43137  relexp0a  43729  ntrclscls00  44079  dvconstbi  44353  expgrowth  44354  addrfv  44488  subrfv  44489  mulvfv  44490  refsum2cnlem1  45042  limcperiod  45643  cncfiooiccre  45910  dvbdfbdioolem1  45943  itgioocnicc  45992  fourierdlem73  46194  fourierdlem82  46203  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  sqwvfoura  46243  etransclem46  46295  nnfoctbdjlem  46470  ovn0  46581  smflim  46792  afveu  47165  afv2eu  47250  fvmptrabdm  47305  imasetpreimafvbijlemfo  47392  lighneallem3  47594  mogoldbblem  47707  fpprel2  47728  sbgoldbwt  47764  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbnd  47796  grimco  47880  cycl3grtri  47914  lmod0rng  48145  lmodvsmdi  48295  lincdifsn  48341  lcoel0  48345  islindeps2  48400  blenn0  48494  nn0sumshdiglemA  48540  itcoval0mpt  48587  rrx2plordisom  48644  aacllem  49320