Theorem sylan9eq 2798

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  sylan9req  2799  sylan9eqr  2800  difeq12  4053  uneq12  4093  ineq12  4143  ssdifim  4198  ifeq12  4479  ifbi  4483  ifeq12da  4494  preq12  4673  prprc  4705  opeq12  4808  eqsnuniex  5283  opthwiener  5428  opthhausdorff0  5432  xpeq12  5611  sosn  5670  nfimad  5973  coi2  6162  funprg  6482  funtpg  6483  funcnvtp  6491  funcnvqp  6492  funimass1  6510  fimadmfoALT  6693  f1orescnv  6725  resdif  6731  fvmpt2  6880  fvmptnf  6891  fveqressseq  6951  oveq12  7278  cbvmpov  7362  ovmpog  7424  fvmpopr2d  7426  caofinvl  7555  eqopi  7858  el2mpocsbcl  7914  fmpoco  7924  mposn  7932  frnsuppeqg  7981  supp0cosupp0  8013  imacosupp  8014  mpocurryd  8074  fvmpocurryd  8076  wrecseq123OLD  8120  rdgsucmptf  8248  frsucmpt  8258  oevn0  8334  oa0r  8357  om1r  8363  oe1m  8365  omass  8400  oeoalem  8416  oeoa  8417  oeoe  8419  qseq12  8545  map0g  8661  xpcomco  8838  sbthlem4  8862  sbthlem5  8863  xpmapenlem  8920  phplem2  8980  phplem3OLD  8991  phplem4OLD  8992  unxpdomlem3  9018  funsnfsupp  9141  ordtypelem7  9272  ttrcltr  9463  cardennn  9730  dfac9  9881  alephsing  10021  axcc3  10183  ac6num  10224  konigthlem  10313  canthp1lem2  10398  ordpipq  10687  ltrnq  10724  addclprlem2  10762  mulclprlem  10764  prlem934  10778  prlem936  10792  mulcmpblnrlem  10815  addcnsr  10880  mulcnsr  10881  axcnre  10909  recex  11596  rpnnen1lem3  12708  rpnnen1lem5  12710  xaddpnf1  12949  xaddpnf2  12950  xaddmnf1  12951  xaddmnf2  12952  rexadd  12955  xnn0xaddcl  12958  xaddnemnf  12959  xaddnepnf  12960  xadddilem  13017  addmodlteq  13655  om2uzrani  13661  om2uzrdg  13665  seqf1olem2  13752  seqf1o  13753  modexp  13942  faclbnd4lem3  13998  hashunsng  14096  hashwrdn  14239  lsw1  14259  swrdfv  14350  swrdccat  14437  ccats1pfxeqbi  14444  revfv  14465  cshwsublen  14498  wrdlen2  14646  wrdl2exs2  14648  wwlktovf1  14661  relexp0  14723  relexpcnv  14735  shftcan1  14783  remul2  14830  immul2  14837  sumss  15425  geomulcvg  15577  fprodss  15647  binomfallfaclem2  15739  bpolylem  15747  ef0lem  15777  efieq1re  15897  rpnnen2lem1  15912  ruclem3  15931  dvdsnegb  15972  dvdscmul  15981  dvds2ln  15987  dvds2add  15988  dvds2sub  15989  gcdn0val  16194  rpmulgcd  16255  lcmn0val  16289  odzval  16481  pcval  16534  pcmpt  16582  prmreclem4  16609  1arithlem2  16614  vdwlem8  16678  ramcl2lem  16699  ramtcl  16700  ramtub  16702  ramcl2  16706  ramcl  16719  setsval  16857  prfcl  17909  curf1cl  17935  curfcl  17939  hofcl  17966  yonedalem4c  17984  psssdm  18289  grplactval  18666  mulgnn0gsum  18699  cntzval  18916  f1omvdco2  19045  pmtrfinv  19058  psgnunilem5  19091  odlem2  19136  gexlem2  19176  lsmvalx  19233  efgtval  19318  efgredlema  19335  vrgpval  19362  cyggex  19488  gsumcom2  19565  fincygsubgodd  19704  dvdsrtr  19883  abvtrivd  20089  lmhmco  20294  reslmhm  20303  lvecinv  20364  zrhmulg  20700  znzrhval  20743  ocvval  20861  mplmon2  21258  subrgasclcl  21264  coe1fv  21366  coe1fzgsumdlem  21461  evl1gsumdlem  21511  mat1dimscm  21613  dmatid  21633  scmatdmat  21653  mavmul0g  21691  1marepvmarrepid  21713  mdetunilem2  21751  gsummatr01lem3  21795  gsummatr01  21797  smadiadetlem3  21806  m2cpminvid2lem  21892  chpdmatlem2  21977  isopn3  22206  cnpval  22376  ptbasfi  22721  dfac14  22758  cnmptkk  22823  xkofvcn  22824  cnmptk1p  22825  cnmptk2  22826  xkocnv  22954  flfval  23130  ptcmplem3  23194  ptcmpg  23197  tmdmulg  23232  prdsxmslem2  23674  subgnm2  23779  nmoval  23868  fsum2cn  24023  pcovalg  24164  isclmp  24249  cphnm  24346  tcphnmval  24382  ovolctb  24643  ioorcl  24730  uniioombllem2  24736  itg1addlem3  24851  itg1climres  24868  itg2uba  24897  itg2splitlem  24902  elcpn  25087  dvexp  25106  dvexp2  25107  rolle  25143  cmvth  25144  mvth  25145  dvlip  25146  dvlipcn  25147  dvlip2  25148  dveq0  25153  dv11cn  25154  lhop1lem  25166  lhop2  25168  lhop  25169  dvcvx  25173  ftc2ditglem  25198  itgsubstlem  25201  ig1pval  25326  elply2  25346  coeid2  25389  coemul  25402  taylthlem2  25522  ulmdvlem1  25548  mtest  25552  pserval2  25559  abelthlem1  25579  abelthlem3  25581  abelthlem8  25587  abelthlem9  25588  pige3ALT  25665  0cxp  25810  leibpi  26081  igamgam  26187  mule1  26286  bposlem5  26425  lgsval3  26452  lgsdinn0  26482  dchrvmasumlem1  26632  dchrisum0flblem1  26645  rpvmasum2  26649  padicval  26754  axsegconlem1  27274  ax5seglem9  27294  axpasch  27298  axeuclidlem  27319  axcontlem2  27322  finsumvtxdg2ssteplem4  27904  usgr2wlkspthlem2  28113  crctcshlem4  28172  wwlknp  28195  wlkiswwlks2lem3  28223  wwlksnred  28244  wwlksnextproplem2  28262  umgrwwlks2on  28309  clwlkclwwlklem2a  28349  clwwisshclwwsn  28367  clwwlknlbonbgr1  28390  clwwlkn1loopb  28394  clwwlkf  28398  clwwlkext2edg  28407  wwlksext2clwwlk  28408  erclwwlknsym  28421  erclwwlkntr  28422  clwwlknon1  28448  clwwlknonex2  28460  eupth2lem3lem3  28581  eucrct2eupth  28596  fusgreghash2wspv  28686  2clwwlk2clwwlklem  28697  2clwwlk2clwwlk  28701  numclwwlk1lem2f1  28708  grpoidinvlem4  28856  grpoinvval  28872  grpodivval  28884  ipval  29052  sspgval  29078  sspsval  29080  sspnval  29086  nmooval  29112  ipasslem1  29180  ipasslem4  29183  hial0  29451  hial02  29452  ocsh  29632  pjhval  29746  hosval  30089  homval  30090  hodval  30091  hfsval  30092  hfmval  30093  braval  30293  kbval  30303  eigvalval  30309  0hmop  30332  adj0  30343  lnopeq0i  30356  nmopcoi  30444  pjclem4  30548  pj3si  30556  hstoh  30581  strlem3a  30601  hstrlem3a  30609  mdexchi  30684  atcv0eq  30728  atcv1  30729  fpwrelmap  31055  cycpmco2lem4  31383  cycpmco2lem5  31384  smatfval  31732  measxun2  32165  measdivcst  32179  measdivcstALTV  32180  ddeval1  32189  ddeval0  32190  ballotlemfp1  32445  signswmnd  32523  signstfvneq0  32538  signstfvc  32540  ftc2re  32565  itgexpif  32573  bnj1128  32957  subfacp1lem3  33131  subfacp1lem5  33133  cvmlift2lem3  33254  msubco  33480  altopthsn  34250  fnetr  34527  fnejoin2  34545  bj-evalid  35234  finxpreclem3  35551  finxpreclem5  35553  finxpreclem6  35554  curf  35742  curunc  35746  matunitlindf  35762  poimirlem4  35768  poimirlem25  35789  mblfinlem2  35802  mblfinlem3  35803  mbfresfi  35810  itg2addnclem  35815  itg2addnc  35818  ftc1anclem5  35841  isbnd3  35929  bndss  35931  grposnOLD  36027  ghomco  36036  xrneq12  36500  lkrval  37089  pmapval  37758  polvalN  37906  watvalN  37994  ldilset  38110  ltrnset  38119  dilsetN  38154  trnsetN  38157  trlset  38162  trlval  38163  cdleme16b  38280  cdleme31fv1  38392  cdlemg1idlemN  38573  tgrpset  38746  tendoset  38760  erngset  38801  erngplus  38804  erngmul  38807  erngset-rN  38809  erngplus-rN  38812  dvaset  39006  dvaplusg  39010  dvamulr  39013  dvavadd  39016  dvavsca  39018  diafval  39032  dvhset  39082  dvhmulr  39087  dvhvadd  39093  dvhvsca  39102  docafvalN  39123  djafvalN  39135  dibfval  39142  dicfval  39176  dihfval  39232  dihval  39233  dihvalc  39234  dihvalb  39238  dochfval  39351  djhfval  39398  lcdval  39590  mapdfval  39628  mapdn0  39670  hvmapfval  39760  hdmap1fval  39797  hdmapfval  39828  hgmapfval  39887  sn-it0e0  40384  pw2f1ocnv  40846  hbtlem7  40937  relexp0a  41284  ntrclscls00  41636  dvconstbi  41912  expgrowth  41913  addrfv  42047  subrfv  42048  mulvfv  42049  refsum2cnlem1  42540  limcperiod  43129  cncfiooiccre  43396  dvbdfbdioolem1  43429  itgioocnicc  43478  fourierdlem73  43680  fourierdlem82  43689  fourierdlem94  43701  fourierdlem103  43710  fourierdlem104  43711  fourierdlem113  43720  sqwvfoura  43729  etransclem46  43781  nnfoctbdjlem  43953  ovn0  44064  smflim  44269  afveu  44602  afv2eu  44687  fvmptrabdm  44742  imasetpreimafvbijlemfo  44814  lighneallem3  45016  mogoldbblem  45129  fpprel2  45150  sbgoldbwt  45186  nnsum4primeseven  45209  nnsum4primesevenALTV  45210  bgoldbtbnd  45218  lmod0rng  45383  rnghmval  45406  lmodvsmdi  45675  lincdifsn  45722  lcoel0  45726  islindeps2  45781  blenn0  45876  nn0sumshdiglemA  45922  itcoval0mpt  45969  rrx2plordisom  46026  aacllem  46462