Theorem sylan9eq 2860

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  sylan9req  2861  sylan9eqr  2862  difeq12  3922  uneq12  3961  ineq12  4008  ssdifim  4064  ifeq12  4296  ifbi  4300  ifeq12da  4311  preq12  4461  prprc  4493  opeq12  4597  opthwiener  5169  opthhausdorff0  5173  xpeq12  5335  sosn  5390  nfimad  5685  coi2  5866  funprg  6154  funtpg  6155  funcnvtp  6163  funcnvqp  6164  funimass1  6182  f1orescnv  6368  resdif  6373  fvmpt2  6512  fvmptnf  6523  fveqressseq  6577  oveq12  6883  cbvmpt2v  6965  ovmpt2g  7025  caofinvl  7154  eqopi  7434  el2mpt2csbcl  7483  fmpt2co  7494  mpt2sn  7502  supp0cosupp0  7569  mpt2curryd  7630  fvmpt2curryd  7632  wrecseq123  7643  rdgsucmptf  7760  frsucmpt  7769  oevn0  7832  oa0r  7855  om1r  7860  oe1m  7862  omass  7897  oeoalem  7913  oeoa  7914  oeoe  7916  map0g  8133  xpcomco  8289  sbthlem4  8312  sbthlem5  8313  xpmapenlem  8366  phplem3  8380  phplem4  8381  unxpdomlem3  8405  funsnfsupp  8538  ordtypelem7  8668  cardennn  9092  dfac9  9243  cdaassen  9289  alephsing  9383  axcc3  9545  ac6num  9586  konigthlem  9675  canthp1lem2  9760  ordpipq  10049  ltrnq  10086  addclprlem2  10124  mulclprlem  10126  prlem934  10140  prlem936  10154  mulcmpblnrlem  10176  addcnsr  10241  mulcnsr  10242  axcnre  10270  recex  10944  rpnnen1lem3  12035  rpnnen1lem5  12037  xaddpnf1  12275  xaddpnf2  12276  xaddmnf1  12277  xaddmnf2  12278  rexadd  12281  xnn0xaddcl  12284  xaddnemnf  12285  xaddnepnf  12286  xadddilem  12342  addmodlteq  12969  om2uzrani  12975  om2uzrdg  12979  seqf1olem2  13064  seqf1o  13065  modexp  13222  faclbnd4lem3  13302  hashunsng  13399  lsw1  13566  swrdfv  13647  swrdccat  13717  ccats1swrdeqbi  13722  revfv  13736  cshwsublen  13766  wrdlen2  13913  wrdl2exs2  13915  wwlktovf1  13925  relexp0  13986  relexpcnv  13998  shftcan1  14046  remul2  14093  immul2  14100  sumss  14678  geomulcvg  14829  fprodss  14899  binomfallfaclem2  14991  bpolylem  14999  ef0lem  15029  efieq1re  15149  rpnnen2lem1  15163  ruclem3  15182  dvdsnegb  15222  dvdscmul  15231  dvds2ln  15237  dvds2add  15238  dvds2sub  15239  gcdn0val  15439  rpmulgcd  15494  lcmn0val  15527  odzval  15713  pcval  15766  pcmpt  15813  prmreclem4  15840  1arithlem2  15845  vdwlem8  15909  ramcl2lem  15930  ramtcl  15931  ramtub  15933  ramcl2  15937  ramcl  15950  setsval  16099  prfcl  17048  curf1cl  17073  curfcl  17077  hofcl  17104  yonedalem4c  17122  psssdm  17421  grplactval  17722  cntzval  17955  f1omvdco2  18069  pmtrfinv  18082  psgnunilem5  18115  odlem2  18159  gexlem2  18198  lsmvalx  18255  efgtval  18337  efgredlema  18354  vrgpval  18381  cyggex  18500  gsumcom2  18575  dvdsrtr  18854  abvtrivd  19044  lmhmco  19250  reslmhm  19259  lvecinv  19320  mplmon2  19701  subrgasclcl  19707  coe1fv  19784  coe1fzgsumdlem  19879  evl1gsumdlem  19928  zrhmulg  20066  znzrhval  20102  ocvval  20221  mat1dimscm  20492  dmatid  20512  scmatdmat  20532  mavmul0g  20570  1marepvmarrepid  20592  mdetunilem2  20630  gsummatr01lem3  20675  gsummatr01  20677  smadiadetlem3  20686  m2cpminvid2lem  20772  chpdmatlem2  20857  isopn3  21084  cnpval  21254  ptbasfi  21598  dfac14  21635  cnmptkk  21700  xkofvcn  21701  cnmptk1p  21702  cnmptk2  21703  xkocnv  21831  flfval  22007  ptcmplem3  22071  ptcmpg  22074  tmdmulg  22109  prdsxmslem2  22547  subgnm2  22651  nmoval  22732  fsum2cn  22887  pcovalg  23024  isclmp  23109  cphnm  23205  tchnmval  23240  ovolctb  23471  ioorcl  23558  uniioombllem2  23564  itg1addlem3  23679  itg1climres  23695  itg2uba  23724  itg2splitlem  23729  elcpn  23911  dvexp  23930  dvexp2  23931  rolle  23967  cmvth  23968  mvth  23969  dvlip  23970  dvlipcn  23971  dvlip2  23972  dveq0  23977  dv11cn  23978  lhop1lem  23990  lhop2  23992  lhop  23993  dvcvx  23997  ftc2ditglem  24022  itgsubstlem  24025  ig1pval  24146  elply2  24166  coeid2  24209  coemul  24222  taylthlem2  24342  ulmdvlem1  24368  mtest  24372  pserval2  24379  abelthlem1  24399  abelthlem3  24401  abelthlem8  24407  abelthlem9  24408  pige3  24484  0cxp  24626  leibpi  24883  igamgam  24989  mule1  25088  bposlem5  25227  lgsval3  25254  lgsdinn0  25284  dchrvmasumlem1  25398  dchrisum0flblem1  25411  rpvmasum2  25415  padicval  25520  axsegconlem1  26011  ax5seglem9  26031  axpasch  26035  axeuclidlem  26056  axcontlem2  26059  finsumvtxdg2ssteplem4  26672  usgr2wlkspthlem2  26882  crctcshlem4  26941  wwlknp  26964  wlkiswwlks2lem3  26998  wwlksnred  27029  wwlksnextproplem2  27048  wspthsnwspthsnonOLD  27056  umgrwwlks2on  27098  clwlkclwwlklem2a  27141  clwwisshclwwsn  27159  clwwlknlbonbgr1  27188  clwwlkn1loopb  27192  clwwlkf  27196  clwwlkext2edg  27206  wwlksext2clwwlkOLD  27208  erclwwlknsym  27221  erclwwlkntr  27222  clwwlknon1  27265  clwwlknonex2  27278  eupth2lem3lem3  27403  eucrct2eupth  27418  fusgreghash2wspv  27510  2clwwlk2clwwlklem  27523  2clwwlk2clwwlk  27527  numclwwlk1lem2f1  27536  grpoidinvlem4  27690  grpoinvval  27706  grpodivval  27718  ipval  27886  sspgval  27912  sspsval  27914  sspnval  27920  nmooval  27946  ipasslem1  28014  ipasslem4  28017  hial0  28287  hial02  28288  ocsh  28470  pjhval  28584  hosval  28927  homval  28928  hodval  28929  hfsval  28930  hfmval  28931  braval  29131  kbval  29141  eigvalval  29147  0hmop  29170  adj0  29181  lnopeq0i  29194  nmopcoi  29282  pjclem4  29386  pj3si  29394  hstoh  29419  strlem3a  29439  hstrlem3a  29447  mdexchi  29522  atcv0eq  29566  atcv1  29567  fpwrelmap  29835  smatfval  30186  measxun2  30598  measdivcstOLD  30612  measdivcst  30613  ddeval1  30622  ddeval0  30623  ballotlemfp1  30878  signswmnd  30959  signstfvneq0  30974  ftc2re  31001  itgexpif  31009  bnj1128  31381  subfacp1lem3  31487  subfacp1lem5  31489  cvmlift2lem3  31610  msubco  31751  altopthsn  32389  fnetr  32667  fnejoin2  32685  bj-evalid  33339  finxpreclem3  33546  finxpreclem5  33548  finxpreclem6  33549  curf  33700  curunc  33704  matunitlindf  33720  poimirlem4  33726  poimirlem25  33747  mblfinlem2  33760  mblfinlem3  33761  mbfresfi  33768  itg2addnclem  33773  itg2addnc  33776  ftc1anclem5  33801  isbnd3  33894  bndss  33896  grposnOLD  33992  ghomco  34001  qseq12  34375  xrneq12  34458  lkrval  34868  pmapval  35537  polvalN  35685  watvalN  35773  ldilset  35889  ltrnset  35898  dilsetN  35934  trnsetN  35937  trlset  35942  trlval  35943  cdleme16b  36060  cdleme31fv1  36172  cdlemg1idlemN  36353  tgrpset  36526  tendoset  36540  erngset  36581  erngplus  36584  erngmul  36587  erngset-rN  36589  erngplus-rN  36592  dvaset  36786  dvaplusg  36790  dvamulr  36793  dvavadd  36796  dvavsca  36798  diafval  36812  dvhset  36862  dvhmulr  36867  dvhvadd  36873  dvhvsca  36882  docafvalN  36903  djafvalN  36915  dibfval  36922  dicfval  36956  dihfval  37012  dihval  37013  dihvalc  37014  dihvalb  37018  dochfval  37131  djhfval  37178  lcdval  37370  mapdfval  37408  mapdn0  37450  hvmapfval  37540  hdmap1fval  37577  hdmapfval  37608  hgmapfval  37667  pw2f1ocnv  38105  hbtlem7  38196  relexp0a  38508  ntrclscls00  38864  dvconstbi  39033  expgrowth  39034  addrfv  39171  subrfv  39172  mulvfv  39173  refsum2cnlem1  39690  limcperiod  40340  cncfiooiccre  40588  dvbdfbdioolem1  40623  itgioocnicc  40672  fourierdlem73  40875  fourierdlem82  40884  fourierdlem94  40896  fourierdlem103  40905  fourierdlem104  40906  fourierdlem113  40915  sqwvfoura  40924  etransclem46  40976  nnfoctbdjlem  41151  ovn0  41262  smflim  41467  afveu  41742  afv2eu  41827  fvmptrabdm  41883  ccats1pfxeqbi  42006  lighneallem3  42099  mogoldbblem  42204  sbgoldbwt  42240  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  bgoldbtbnd  42272  lmod0rng  42436  rnghmval  42459  lmodvsmdi  42731  lincdifsn  42781  lcoel0  42785  islindeps2  42840  blenn0  42935  nn0sumshdiglemA  42981  aacllem  43118