Theorem sylan9eq 2794

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 596	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  sylan9req  2795  sylan9eqr  2796  difeq12  4130  uneq12  4172  ineq12  4222  ssdifim  4278  ifeq12  4548  ifbi  4552  ifeq12da  4563  preq12  4739  prprc  4771  opeq12  4879  eqsnuniex  5366  opthwiener  5523  opthhausdorff0  5527  xpeq12  5713  sosn  5774  nfimad  6088  coi2  6284  funprg  6621  funtpg  6622  funcnvtp  6630  funcnvqp  6631  funimass1  6649  fimadmfoALT  6831  f1orescnv  6863  resdif  6869  fvmpt2  7026  fvmptnf  7037  fveqressseq  7098  oveq12  7439  cbvmpov  7527  ovmpog  7591  fvmpopr2d  7594  caofinvl  7728  eqopi  8048  el2mpocsbcl  8108  fmpoco  8118  mposn  8126  fsuppeqg  8199  supp0cosupp0  8231  imacosupp  8232  mpocurryd  8292  fvmpocurryd  8294  wrecseq123OLD  8338  rdgsucmptf  8466  frsucmpt  8476  oevn0  8551  oa0r  8574  om1r  8579  oe1m  8581  omass  8616  oeoalem  8632  oeoa  8633  oeoe  8635  qseq12  8804  map0g  8922  xpcomco  9100  sbthlem4  9124  sbthlem5  9125  xpmapenlem  9182  phplem2  9242  phplem3OLD  9253  phplem4OLD  9254  unxpdomlem3  9285  funsnfsupp  9429  ordtypelem7  9561  ttrcltr  9753  cardennn  10020  dfac9  10174  alephsing  10313  axcc3  10475  ac6num  10516  konigthlem  10605  canthp1lem2  10690  ordpipq  10979  ltrnq  11016  addclprlem2  11054  mulclprlem  11056  prlem934  11070  prlem936  11084  mulcmpblnrlem  11107  addcnsr  11172  mulcnsr  11173  axcnre  11201  recex  11892  rpnnen1lem3  13018  rpnnen1lem5  13020  xaddpnf1  13264  xaddpnf2  13265  xaddmnf1  13266  xaddmnf2  13267  rexadd  13270  xnn0xaddcl  13273  xaddnemnf  13274  xaddnepnf  13275  xadddilem  13332  addmodlteq  13983  om2uzrani  13989  om2uzrdg  13993  seqf1olem2  14079  seqf1o  14080  modexp  14273  faclbnd4lem3  14330  hashunsng  14427  hashwrdn  14581  lsw1  14601  swrdfv  14682  swrdccat  14769  ccats1pfxeqbi  14776  revfv  14797  cshwsublen  14830  wrdlen2  14979  wrdl2exs2  14981  wwlktovf1  14992  relexp0  15058  relexpcnv  15070  shftcan1  15118  remul2  15165  immul2  15172  sumss  15756  geomulcvg  15908  fprodss  15980  binomfallfaclem2  16072  bpolylem  16080  ef0lem  16110  efieq1re  16231  rpnnen2lem1  16246  ruclem3  16265  dvdsnegb  16307  dvdscmul  16316  dvds2ln  16322  dvds2add  16323  dvds2sub  16324  gcdn0val  16531  rpmulgcd  16590  lcmn0val  16628  odzval  16824  pcval  16877  pcmpt  16925  prmreclem4  16952  1arithlem2  16957  vdwlem8  17021  ramcl2lem  17042  ramtcl  17043  ramtub  17045  ramcl2  17049  ramcl  17062  setsval  17200  prfcl  18258  curf1cl  18284  curfcl  18288  hofcl  18315  yonedalem4c  18333  psssdm  18639  grplactval  19072  mulgnn0gsum  19110  cntzval  19351  f1omvdco2  19480  pmtrfinv  19493  psgnunilem5  19526  odlem2  19571  gexlem2  19614  lsmvalx  19671  efgtval  19755  efgredlema  19772  vrgpval  19799  cyggex  19930  gsumcom2  20007  fincygsubgodd  20146  dvdsrtr  20384  rnghmval  20456  abvtrivd  20849  lmhmco  21059  reslmhm  21068  lvecinv  21132  zrhmulg  21537  znzrhval  21582  ocvval  21702  mplmon2  22102  subrgasclcl  22108  coe1fv  22223  coe1fzgsumdlem  22322  evl1gsumdlem  22375  mat1dimscm  22496  dmatid  22516  scmatdmat  22536  mavmul0g  22574  1marepvmarrepid  22596  mdetunilem2  22634  gsummatr01lem3  22678  gsummatr01  22680  smadiadetlem3  22689  m2cpminvid2lem  22775  chpdmatlem2  22860  isopn3  23089  cnpval  23259  ptbasfi  23604  dfac14  23641  cnmptkk  23706  xkofvcn  23707  cnmptk1p  23708  cnmptk2  23709  xkocnv  23837  flfval  24013  ptcmplem3  24077  ptcmpg  24080  tmdmulg  24115  prdsxmslem2  24557  subgnm2  24662  nmoval  24751  fsum2cn  24908  pcovalg  25058  isclmp  25143  cphnm  25240  tcphnmval  25276  ovolctb  25538  ioorcl  25625  uniioombllem2  25631  itg1addlem3  25746  itg1climres  25763  itg2uba  25792  itg2splitlem  25797  elcpn  25984  dvexp  26005  dvexp2  26006  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvlipcn  26047  dvlip2  26048  dveq0  26053  dv11cn  26054  lhop1lem  26066  lhop2  26068  lhop  26069  dvcvx  26073  ftc2ditglem  26100  itgsubstlem  26103  ig1pval  26229  elply2  26249  coeid2  26292  coemul  26305  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem1  26457  mtest  26461  pserval2  26468  abelthlem1  26489  abelthlem3  26491  abelthlem8  26497  abelthlem9  26498  pige3ALT  26576  0cxp  26722  leibpi  26999  igamgam  27106  mule1  27205  bposlem5  27346  lgsval3  27373  lgsdinn0  27403  dchrvmasumlem1  27553  dchrisum0flblem1  27566  rpvmasum2  27570  padicval  27675  abssid  28279  abssnid  28281  cutpw2  28431  axsegconlem1  28946  ax5seglem9  28966  axpasch  28970  axeuclidlem  28991  axcontlem2  28994  finsumvtxdg2ssteplem4  29580  usgr2wlkspthlem2  29790  crctcshlem4  29849  wwlknp  29872  wlkiswwlks2lem3  29900  wwlksnred  29921  wwlksnextproplem2  29939  umgrwwlks2on  29986  clwlkclwwlklem2a  30026  clwwisshclwwsn  30044  clwwlknlbonbgr1  30067  clwwlkn1loopb  30071  clwwlkf  30075  clwwlkext2edg  30084  wwlksext2clwwlk  30085  erclwwlknsym  30098  erclwwlkntr  30099  clwwlknon1  30125  clwwlknonex2  30137  eupth2lem3lem3  30258  eucrct2eupth  30273  fusgreghash2wspv  30363  2clwwlk2clwwlklem  30374  2clwwlk2clwwlk  30378  numclwwlk1lem2f1  30385  grpoidinvlem4  30535  grpoinvval  30551  grpodivval  30563  ipval  30731  sspgval  30757  sspsval  30759  sspnval  30765  nmooval  30791  ipasslem1  30859  ipasslem4  30862  hial0  31130  hial02  31131  ocsh  31311  pjhval  31425  hosval  31768  homval  31769  hodval  31770  hfsval  31771  hfmval  31772  braval  31972  kbval  31982  eigvalval  31988  0hmop  32011  adj0  32022  lnopeq0i  32035  nmopcoi  32123  pjclem4  32227  pj3si  32235  hstoh  32260  strlem3a  32280  hstrlem3a  32288  mdexchi  32363  atcv0eq  32407  atcv1  32408  fpwrelmap  32750  cycpmco2lem4  33131  cycpmco2lem5  33132  smatfval  33755  measxun2  34190  measdivcst  34204  measdivcstALTV  34205  ddeval1  34214  ddeval0  34215  ballotlemfp1  34472  signswmnd  34550  signstfvneq0  34565  signstfvc  34567  ftc2re  34591  itgexpif  34599  bnj1128  34982  subfacp1lem3  35166  subfacp1lem5  35168  cvmlift2lem3  35289  msubco  35515  altopthsn  35942  ditgeq12d  36204  fnetr  36333  fnejoin2  36351  bj-evalid  37058  finxpreclem3  37375  finxpreclem5  37377  finxpreclem6  37378  curf  37584  curunc  37588  matunitlindf  37604  poimirlem4  37610  poimirlem25  37631  mblfinlem2  37644  mblfinlem3  37645  mbfresfi  37652  itg2addnclem  37657  itg2addnc  37660  ftc1anclem5  37683  isbnd3  37770  bndss  37772  grposnOLD  37868  ghomco  37877  xrneq12  38364  lkrval  39069  pmapval  39739  polvalN  39887  watvalN  39975  ldilset  40091  ltrnset  40100  dilsetN  40135  trnsetN  40138  trlset  40143  trlval  40144  cdleme16b  40261  cdleme31fv1  40373  cdlemg1idlemN  40554  tgrpset  40727  tendoset  40741  erngset  40782  erngplus  40785  erngmul  40788  erngset-rN  40790  erngplus-rN  40793  dvaset  40987  dvaplusg  40991  dvamulr  40994  dvavadd  40997  dvavsca  40999  diafval  41013  dvhset  41063  dvhmulr  41068  dvhvadd  41074  dvhvsca  41083  docafvalN  41104  djafvalN  41116  dibfval  41123  dicfval  41157  dihfval  41213  dihval  41214  dihvalc  41215  dihvalb  41219  dochfval  41332  djhfval  41379  lcdval  41571  mapdfval  41609  mapdn0  41651  hvmapfval  41741  hdmap1fval  41778  hdmapfval  41809  hgmapfval  41868  fmpocos  42253  sn-it0e0  42421  zaddcomlem  42457  pw2f1ocnv  43025  hbtlem7  43113  relexp0a  43705  ntrclscls00  44055  dvconstbi  44329  expgrowth  44330  addrfv  44464  subrfv  44465  mulvfv  44466  refsum2cnlem1  44974  limcperiod  45583  cncfiooiccre  45850  dvbdfbdioolem1  45883  itgioocnicc  45932  fourierdlem73  46134  fourierdlem82  46143  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  sqwvfoura  46183  etransclem46  46235  nnfoctbdjlem  46410  ovn0  46521  smflim  46732  afveu  47102  afv2eu  47187  fvmptrabdm  47242  imasetpreimafvbijlemfo  47329  lighneallem3  47531  mogoldbblem  47644  fpprel2  47665  sbgoldbwt  47701  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbnd  47733  grimco  47817  lmod0rng  48072  lmodvsmdi  48223  lincdifsn  48269  lcoel0  48273  islindeps2  48328  blenn0  48422  nn0sumshdiglemA  48468  itcoval0mpt  48515  rrx2plordisom  48572  aacllem  49031