Theorem sylan9eq 2820

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  sylan9req  2821  sylan9eqr  2822  difeq12  4076  uneq12  4117  ineq12  4168  ssdifim  4226  ifeq12  4508  ifbi  4512  ifeq12da  4523  preq12  4703  prprc  4735  opeq12  4842  eqsnuniex  5334  opthwiener  5499  opthhausdorff0  5503  xpeq12  5688  sosn  5750  nfimad  6073  coi2  6267  funprg  6594  funtpg  6595  funcnvtp  6603  funcnvqp  6604  funimass1  6622  fimadmfoALT  6807  f1orescnv  6840  resdif  6846  fvmpt2  7005  fvmptnf  7016  fveqressseq  7078  oveq12  7428  cbvmpov  7514  ovmpog  7578  fvmpopr2d  7581  caofinvl  7716  eqopi  8028  el2mpocsbcl  8086  fmpoco  8096  mposn  8104  fsuppeqg  8178  supp0cosupp0  8210  imacosupp  8211  mpocurryd  8271  fvmpocurryd  8273  rdgsucmptf  8421  frsucmpt  8431  oevn0  8506  oa0r  8529  om1r  8534  oe1m  8536  omass  8571  oeoalem  8588  oeoa  8589  oeoe  8591  qseq12  8765  map0g  8888  xpcomco  9062  sbthlem4  9085  sbthlem5  9086  xpmapenlem  9139  phplem2  9196  unxpdomlem3  9225  funsnfsupp  9359  ordtypelem7  9493  ttrcltr  9692  cardennn  9985  dfac9  10136  alephsing  10275  axcc3  10437  ac6num  10478  konigthlem  10568  canthp1lem2  10653  ordpipq  10942  ltrnq  10979  addclprlem2  11017  mulclprlem  11019  prlem934  11033  prlem936  11047  mulcmpblnrlem  11070  addcnsr  11135  mulcnsr  11136  axcnre  11164  recex  11861  rpnnen1lem3  13019  rpnnen1lem5  13021  xaddpnf1  13268  xaddpnf2  13269  xaddmnf1  13270  xaddmnf2  13271  rexadd  13274  xnn0xaddcl  13277  xaddnemnf  13278  xaddnepnf  13279  xadddilem  13336  addmodlteq  14000  om2uzrani  14006  om2uzrdg  14010  seqf1olem2  14096  seqf1o  14097  modexp  14292  faclbnd4lem3  14349  hashunsng  14446  hashwrdn  14602  lsw1  14622  swrdfv  14706  swrdccat  14794  ccats1pfxeqbi  14801  revfv  14822  cshwsublen  14857  wrdlen2  15005  wrdl2exs2  15007  wwlktovf1  15018  relexp0  15084  relexpcnv  15096  shftcan1  15144  remul2  15205  immul2  15212  sumss  15798  geomulcvg  15953  fprodss  16025  binomfallfaclem2  16116  bpolylem  16124  ef0lem  16154  efieq1re  16277  rpnnen2lem1  16292  ruclem3  16311  dvdsnegb  16353  dvdscmul  16362  dvds2ln  16369  dvds2add  16370  dvds2sub  16371  gcdn0val  16578  rpmulgcd  16637  lcmn0val  16675  odzval  16873  pcval  16926  pcmpt  16974  prmreclem4  17001  1arithlem2  17006  vdwlem8  17070  ramcl2lem  17091  ramtcl  17092  ramtub  17094  ramcl2  17098  ramcl  17111  setsval  17249  prfcl  18281  curf1cl  18306  curfcl  18310  hofcl  18337  yonedalem4c  18355  psssdm  18660  chneq12  18692  grplactval  19152  mulgnn0gsum  19190  cntzval  19435  f1omvdco2  19562  pmtrfinv  19575  psgnunilem5  19608  odlem2  19653  gexlem2  19696  lsmvalx  19753  efgtval  19837  efgredlema  19854  vrgpval  19881  cyggex  20012  gsumcom2  20089  fincygsubgodd  20228  dvdsrtr  20496  rnghmval  20568  abvtrivd  20985  lmhmco  21214  reslmhm  21223  lvecinv  21287  zrhmulg  21709  znzrhval  21746  ocvval  21867  mplmon2  22262  subrgasclcl  22268  coe1fv  22416  coe1fzgsumdlem  22513  evl1gsumdlem  22566  mat1dimscm  22682  dmatid  22702  scmatdmat  22722  mavmul0g  22760  1marepvmarrepid  22782  mdetunilem2  22820  gsummatr01lem3  22864  gsummatr01  22866  smadiadetlem3  22875  m2cpminvid2lem  22961  chpdmatlem2  23046  isopn3  23273  cnpval  23443  ptbasfi  23789  dfac14  23826  cnmptkk  23891  xkofvcn  23892  cnmptk1p  23893  cnmptk2  23894  xkocnv  24022  flfval  24198  ptcmplem3  24262  ptcmpg  24265  tmdmulg  24300  prdsxmslem2  24737  subgnm2  24842  nmoval  24923  fsum2cn  25081  pcovalg  25222  isclmp  25307  cphnm  25403  tcphnmval  25439  ovolctb  25700  ioorcl  25787  uniioombllem2  25793  itg1addlem3  25908  itg1climres  25924  itg2uba  25953  itg2splitlem  25958  elcpn  26144  dvexp  26163  dvexp2  26164  rolle  26200  cmvth  26201  mvth  26202  dvlip  26203  dvlipcn  26204  dvlip2  26205  dveq0  26210  dv11cn  26211  lhop1lem  26223  lhop2  26225  lhop  26226  dvcvx  26230  ftc2ditglem  26255  itgsubstlem  26258  ig1pval  26384  elply2  26404  coeid2  26447  coemul  26460  taylthlem2  26588  ulmdvlem1  26614  mtest  26618  pserval2  26625  abelthlem1  26645  abelthlem3  26647  abelthlem8  26653  abelthlem9  26654  pige3ALT  26736  0cxp  26882  leibpi  27158  igamgam  27264  mule1  27363  bposlem5  27503  lgsval3  27530  lgsdinn0  27560  dchrvmasumlem1  27710  dchrisum0flblem1  27723  rpvmasum2  27727  padicval  27832  abssid  28485  abssnid  28487  axsegconlem1  29322  ax5seglem9  29342  axpasch  29346  axeuclidlem  29367  axcontlem2  29370  finsumvtxdg2ssteplem4  29956  usgr2wlkspthlem2  30171  crctcshlem4  30236  wwlknp  30259  wlkiswwlks2lem3  30287  wwlksnred  30308  wwlksnextproplem2  30326  usgrwwlks2on  30374  umgrwwlks2on  30375  clwlkclwwlklem2a  30416  clwwisshclwwsn  30434  clwwlknlbonbgr1  30457  clwwlkn1loopb  30461  clwwlkf  30465  clwwlkext2edg  30474  wwlksext2clwwlk  30475  erclwwlknsym  30488  erclwwlkntr  30489  clwwlknon1  30515  clwwlknonex2  30527  eupth2lem3lem3  30652  eucrct2eupth  30667  fusgreghash2wspv  30757  2clwwlk2clwwlklem  30768  2clwwlk2clwwlk  30772  numclwwlk1lem2f1  30779  grpoidinvlem4  30930  grpoinvval  30946  grpodivval  30958  ipval  31126  sspgval  31152  sspsval  31154  sspnval  31160  nmooval  31186  ipasslem1  31254  ipasslem4  31257  hial0  31525  hial02  31526  ocsh  31706  pjhval  31820  hosval  32163  homval  32164  hodval  32165  hfsval  32166  hfmval  32167  braval  32367  kbval  32377  eigvalval  32383  0hmop  32406  adj0  32417  lnopeq0i  32430  nmopcoi  32518  pjclem4  32622  pj3si  32630  hstoh  32655  strlem3a  32675  hstrlem3a  32683  mdexchi  32758  atcv0eq  32802  atcv1  32803  fpwrelmap  33148  cycpmco2lem4  33513  cycpmco2lem5  33514  fxpgaval  33551  smatfval  34249  measxun2  34665  measdivcst  34679  measdivcstALTV  34680  ddeval1  34689  ddeval0  34690  ballotlemfp1  34947  signswmnd  35009  signstfvneq0  35024  signstfvc  35026  ftc2re  35050  itgexpif  35058  bnj1128  35443  subfacp1lem3  35711  subfacp1lem5  35713  cvmlift2lem3  35834  msubco  36060  altopthsn  36490  ditgeq12d  36791  fnetr  36919  fnejoin2  36937  ttcsntrsucg  37090  bj-evalid  37775  finxpreclem3  38096  finxpreclem5  38098  finxpreclem6  38099  curf  38306  curunc  38310  matunitlindf  38326  poimirlem4  38332  poimirlem25  38353  mblfinlem2  38366  mblfinlem3  38367  mbfresfi  38374  itg2addnclem  38379  itg2addnc  38382  ftc1anclem5  38405  isbnd3  38493  bndss  38495  grposnOLD  38591  ghomco  38600  xrneq12  39109  lkrval  39920  pmapval  40589  polvalN  40737  watvalN  40825  ldilset  40941  ltrnset  40950  dilsetN  40985  trnsetN  40988  trlset  40993  trlval  40994  cdleme16b  41111  cdleme31fv1  41223  cdlemg1idlemN  41404  tgrpset  41577  tendoset  41591  erngset  41632  erngplus  41635  erngmul  41638  erngset-rN  41640  erngplus-rN  41643  dvaset  41837  dvaplusg  41841  dvamulr  41844  dvavadd  41847  dvavsca  41849  diafval  41863  dvhset  41913  dvhmulr  41918  dvhvadd  41924  dvhvsca  41933  docafvalN  41954  djafvalN  41966  dibfval  41973  dicfval  42007  dihfval  42063  dihval  42064  dihvalc  42065  dihvalb  42069  dochfval  42182  djhfval  42229  lcdval  42421  mapdfval  42459  mapdn0  42501  hvmapfval  42591  hdmap1fval  42628  hdmapfval  42659  hgmapfval  42718  fmpocos  43062  sn-it0e0  43235  zaddcomlem  43295  pw2f1ocnv  43822  hbtlem7  43910  relexp0a  44500  ntrclscls00  44850  dvconstbi  45102  expgrowth  45103  addrfv  45235  subrfv  45236  mulvfv  45237  refsum2cnlem1  45815  limcperiod  46402  cncfiooiccre  46667  dvbdfbdioolem1  46700  itgioocnicc  46749  fourierdlem73  46951  fourierdlem82  46960  fourierdlem94  46972  fourierdlem103  46981  fourierdlem104  46982  fourierdlem113  46991  sqwvfoura  47000  etransclem46  47052  nnfoctbdjlem  47227  ovn0  47338  smflim  47549  afveu  47948  afv2eu  48033  fvmptrabdm  48088  imasetpreimafvbijlemfo  48212  lighneallem3  48417  ppivalnnprm  48435  mogoldbblem  48543  fpprel2  48564  sbgoldbwt  48600  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  bgoldbtbnd  48632  grimco  48712  cycl3grtri  48770  lmod0rng  49051  lmodvsmdi  49216  lincdifsn  49261  lcoel0  49265  islindeps2  49320  blenn0  49410  nn0sumshdiglemA  49456  itcoval0mpt  49503  rrx2plordisom  49560  nelsubclem  49902  aacllem  50678