Theorem sylan9eqr 2820

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)

Hypotheses

Ref	Expression
sylan9eqr.1	⊢ (𝜑 → 𝐴 = 𝐵)
sylan9eqr.2	⊢ (𝜓 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sylan9eqr	⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Proof of Theorem sylan9eqr

Step	Hyp	Ref	Expression
1		sylan9eqr.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sylan9eqr.2	. . 3 ⊢ (𝜓 → 𝐵 = 𝐶)
3	1, 2	sylan9eq 2818	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	3	ancoms 463	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  sbcied2  3788  csbied2  3890  opthhausdorff0  5501  fun2ssres  6581  fcoi1  6752  fcoi2  6753  funssfv  6902  fvtp1  7193  nvof1o  7278  onuninsuci  7832  ot1stg  7996  ot2ndg  7997  el2xptp0  8029  mpomptsx  8057  dmmpossx  8059  fmpox  8060  2ndconst  8092  offsplitfpar  8110  mpoxopoveq  8211  rdgeq12  8396  rdgsucmptnf  8412  frsucmptn  8422  oev2  8504  oesuclem  8506  oawordeulem  8535  om00  8556  omass  8561  omeulem1  8563  oeoa  8579  oeoe  8581  nnmass  8606  oaabs2  8631  omabs  8633  mapsnend  9029  omxpenlem  9062  sbthlem4  9074  sbthlem6  9076  fodomr  9112  ssenen  9135  fodomfir  9283  fi0  9376  cantnfp1  9646  cnfcomlem  9664  ttrclselem2  9691  cardaleph  10069  cflim2  10242  axdc4lem  10434  fpwwe2lem11  10621  fpwwe2lem12  10622  rankcf  10757  inatsk  10758  ltrnq  10959  addclprlem1  10996  mulclprlem  10999  1idpr  11009  prlem936  11027  reclem3pr  11029  mulcmpblnrlem  11050  recexsrlem  11083  map2psrpr  11090  addid0  11628  subdivcomb2  11906  nnadd1com  12254  nnnn0addcl  12529  zindd  12692  qaddcl  12984  qmulcl  12986  qreccl  12988  xaddnemnf  13257  xaddnepnf  13258  xaddcom  13261  xnegdi  13269  xaddass  13270  xpncan  13272  xleadd1a  13274  xlt2add  13281  rexmul  13292  xmulgt0  13304  xmulge0  13305  xmulasslem3  13307  xlemul1a  13309  xadddilem  13315  xadddi2  13318  modmuladd  13945  modm1p1mod0  13954  modfzo0difsn  13975  seqf1olem2  14074  expp1  14100  expneg  14101  expcllem  14104  mulexp  14133  expmul  14139  sqoddm1div8  14275  bcpasc  14353  hashrabsn01  14405  fseq1hash  14408  hashinfxadd  14417  hashfzo  14462  fnfz0hash  14479  ffzo0hash  14482  hashf1lem1  14488  hashge2el2dif  14513  hash3tpexb  14527  hashdifsnp1  14539  lsw0  14598  ccatval1  14610  ccatval2  14611  swrdval  14677  ccatopth  14749  reuccatpfxs1  14780  splval  14784  repswswrd  14817  2cshwcshw  14858  s4dom  14952  wrdlen2i  14975  shftfn  15106  reim0b  15166  cjexp  15197  sqeqd  15213  fsumser  15777  sumsnf  15790  binomlem  15879  expcnv  15914  prodsn  16012  prodsnf  16014  bpolylem  16097  bpoly2  16106  bpoly3  16107  ef0lem  16127  dvdsnegb  16326  mod2eq1n2dvds  16400  m1expe  16427  m1expo  16428  m1exp1  16429  flodddiv4  16468  sadadd2lem2  16503  bezoutr1  16622  dvdslcm  16651  lcmeq0  16653  lcmcl  16654  lcmabs  16658  lcmgcdlem  16659  lcmdvds  16661  lcmf0val  16675  lcmftp  16689  lcmfunsnlem2  16693  mulgcddvds  16708  divgcdcoprmex  16719  pcge0  16917  pcadd  16944  pcmpt2  16948  prmreclem4  16974  ramval  17063  ramcl  17084  fvprmselelfz  17099  fvprmselgcd1  17100  ressid2  17289  ressval2  17290  mndind  18882  frmdval  18905  efmnd  18924  smndex1igid  18960  smndex1igidOLD  18961  smndex1n0mnd  18969  mgm2nsgrplem3  18977  mulgfval  19130  mulgfvalALT  19131  mulgnn0subcl  19148  mulgnn0z  19162  cycsubm  19268  f1ghm0to0  19310  isga  19356  symgextfve  19484  symgfixf1  19502  f1omvdco2  19513  psgnsn  19585  odid  19603  gexid  19646  efgsval2  19798  frgpuptinv  19836  frgpup2  19841  dprdsn  20103  srgmulgass  20294  srgpcomp  20295  srgbinomlem4  20306  ringinvnzdiv  20380  rngcval  20717  ringcval  20746  isabvd  20915  issrng  20947  lmodvsmmulgdi  21018  mptscmfsupp0  21048  lvecinv  21237  lspdisj2  21251  lspfixed  21252  lspexch  21253  sralem  21297  srasca  21301  sravsca  21302  sraip  21303  znval  21685  psgndiflemB  21750  isphl  21778  assamulgscmlem2  22050  mplval  22138  opsrval  22197  psdmvr  22332  cply1mul  22456  gsummoncoe1  22468  evl1fval  22488  scmate  22667  scmatscm  22670  mdetdiagid  22757  mdetunilem7  22775  mdetuni0  22778  gsummatr01lem3  22814  gsummatr01lem4  22815  gsummatr01  22816  slesolinvbi  22838  cpmatacl  22873  cpmatinvcl  22874  pmatcollpw2lem  22934  monmatcollpw  22936  pmatcollpwfi  22939  mp2pm2mplem4  22966  pm2mp  22982  cpmadugsumlemF  23033  cpmadugsumfi  23034  cpmadumatpoly  23040  cayhamlem4  23045  cayleyhamilton0  23046  cayleyhamiltonALT  23048  indistopon  23158  0ntr  23228  pnrmopn  23500  reftr  23671  kgenval  23692  pt1hmeo  23963  fmval  24100  fmf  24102  istmd  24231  istgp  24234  tsmsval2  24287  isxmet2d  24484  xpsxmetlem  24536  xpsmet  24539  blfvalps  24540  tmsval  24638  isnlm  24832  nmoleub  24888  idnghm  24900  blssioo  24952  blcvx  24955  icccvx  25109  pcorevlem  25185  isclm  25223  caufval  25434  iscms  25504  mbfsup  25823  i1f1  25849  dvexp3  26137  rolle  26149  dvivth  26169  deg1add  26260  0dgr  26402  coefv0  26405  elqaalem2  26481  dvradcnv  26584  abelthlem8  26602  efper  26644  logtayl  26825  abscxpbnd  26918  relogbcxpb  26952  logbgcd1irr  26959  dcubic2  27009  rlimcnp2  27131  cvxcl  27149  zetacvg  27179  lgamgulmlem2  27194  vmaval  27277  chtub  27376  logexprlim  27389  dchrsum2  27432  sumdchr2  27434  bposlem2  27449  lgsdir  27496  lgsne0  27499  lgsdirnn0  27508  lgsdinn0  27509  lgsquadlem2  27545  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2lgslem3a1  27564  2lgslem3b1  27565  2lgslem3c1  27566  2lgslem3d1  27567  2sqn0  27598  dchrvmasum2if  27661  dchrvmasumiflem1  27665  rpvmasum2  27676  pntpbnd1  27750  ostth2lem4  27800  expsp1  28622  trgcgrg  28784  tgcgr4  28800  ax5seglem1  29278  ax5seglem2  29279  ax5seglem5  29283  usgr1vr  29605  cplgr2vpr  29783  cplgr3v  29785  cusgrrusgr  29931  wlklenvm1  29971  wlk0prc  30002  wlksoneq1eq2  30012  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  crctcshlem4  30169  crctcsh  30173  wlkiswwlks1  30216  wwlksnext  30242  wwlksnextbi  30243  wwlksnextwrd  30246  midwwlks2s3  30301  clwlkclwwlklem2fv1  30346  clwlkclwwlklem2a4  30348  clwlkclwwlklem3  30352  clwwisshclwws  30366  erclwwlkeqlen  30370  clwwlkinwwlk  30391  clwwlkn2  30395  clwwlkf  30398  clwwlkf1  30400  eleclclwwlknlem2  30412  erclwwlkneqlen  30419  umgrhashecclwwlk  30429  eucrctshift  30594  eucrct2eupth  30596  fusgr2wsp2nb  30685  grpoidinvlem2  30857  vcz  30927  nvz  31021  lnon0  31150  ipasslem2  31184  htthlem  31269  hvpncan  31391  hiidge0  31450  normgt0  31479  hsn0elch  31600  shsel3  31667  spansneleq  31922  normcan  31928  h1datomi  31933  fh1  31970  spansncvi  32004  5oalem1  32006  5oalem3  32008  5oalem5  32010  3oalem2  32015  pjdsi  32064  kbpj  32308  0hmop  32335  0lnfn  32337  adj0  32346  nlelshi  32412  branmfn  32457  opsqrlem1  32492  hst1h  32579  mdsl0  32662  superpos  32706  sumdmdlem  32770  cdj3lem1  32786  f1od2  33064  xrpxdivcld  33254  xrge0npcan  33340  elrgspnlem2  33563  rlocf1  33594  resvid2  33650  resvval2  33651  qsdrng  33779  r1pquslmic  33900  0mplrim  33904  selvply1rhmlemb  33909  selvply1rhmlem2  33911  selvply1rhmlem4  33913  mplvrpmmhm  33936  mplvrpmrhm  33937  esplyfval0  33954  esplyfvaln  33964  vietalem  33969  rtelextdg2lem  34116  esumsnf  34454  esummulc1  34471  measxun2  34600  omsmeas  34713  sibfof  34730  probun  34809  signstfvn  34956  bnj517  35273  pthhashvtx  35620  ex-sategoelel  35913  mrsubfval  36000  msrval  36030  dfrdg2  36285  itgeq12i  36718  bj-prmoore  37757  bj-bary1lem1  37955  rdgeqoa  38016  finxpreclem2  38036  finxpreclem3  38039  matunitlindflem1  38267  poimirlem1  38272  poimirlem2  38273  poimirlem3  38274  poimirlem4  38275  poimirlem5  38276  poimirlem6  38277  poimirlem7  38278  poimirlem10  38281  poimirlem11  38282  poimirlem12  38283  poimirlem14  38285  poimirlem15  38286  poimirlem17  38288  poimirlem20  38291  poimirlem22  38293  poimirlem23  38294  poimirlem24  38295  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  mblfinlem2  38309  mblfinlem3  38310  ismblfin  38312  mbfposadd  38318  itg2addnclem  38322  itg2addnclem3  38324  itg2addnc  38325  ftc1anclem8  38351  areacirc  38364  ismtyval  38451  ismrer1  38489  grposnOLD  38533  rabeq12f  38806  csbeq12  38807  iuneq12f  38812  lsatcv1  39822  glbconN  40151  atltcvr  40209  3dim2  40242  islln2a  40291  2at0mat0  40299  islpln2a  40322  islvol2aN  40366  pmodlem2  40621  pmapjat1  40627  pcl0bN  40697  osumclN  40741  pexmidALTN  40752  lhp2at0nle  40809  4atexlemunv  40840  cdleme18b  41066  cdleme31sn1  41155  cdleme31sde  41159  cdleme31sn2  41163  ltrniotavalbN  41358  trljco  41514  cdlemh  41591  cdlemk40t  41692  cdlemk40f  41693  cdleml9  41758  dihmeetlem3N  42079  dochkrshp  42160  dihprrn  42200  dihjat1  42203  dvh3dim  42220  dochkrsm  42232  dochexmid  42242  lcfl7lem  42273  lcfl9a  42279  lclkrlem1  42280  mapdspex  42442  mapdindp2  42495  mapdh6dN  42513  hdmap1l6d  42587  hdmap11lem2  42616  hdmap14lem4a  42645  hdmapip0  42689  hlhilset  42708  mulgt0b2d  43252  fiabv  43304  prjspner1  43358  0prjspnrel  43359  jm2.26a  43727  onov0suclim  44001  oe0suclim  44004  cantnfresb  44051  onmcl  44058  omcl2  44060  tfsconcatun  44064  naddwordnexlem4  44128  mnringmulrcld  44952  radcnvrat  45024  sumsnd  45746  icccncfext  46601  fperdvper  46633  dvcosax  46640  ioodvbdlimc1lem1  46645  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  volioc  46686  itgiccshift  46694  stoweidlem34  46748  dirkercncflem2  46818  fourierdlem32  46853  fourierdlem41  46862  fourierdlem48  46868  fourierdlem64  46884  fourierdlem73  46893  fourierdlem79  46899  fourierdlem82  46902  fourierdlem97  46917  fourierdlem101  46921  fourierdlem109  46929  fourierdlem111  46931  fouriersw  46945  elaa2  46948  etransclem24  46972  etransclem25  46973  etransclem46  46994  nnfoctbdjlem  47169  ismeannd  47181  smfpimltxr  47461  smfpimgtxr  47494  ndfatafv2undef  47949  fzopredsuc  48061  m1modmmod  48101  modlt0b  48106  prproropf1olem3  48254  prproropf1olem4  48255  fmtnorec2lem  48294  2pwp1prmfmtno  48342  sfprmdvdsmersenne  48355  sgprmdvdsmersenne  48356  lighneallem2  48358  lighneallem3  48359  ppivalnnprm  48377  ppivalnnnprmge6  48378  dfodd6  48402  dfeven4  48403  m1expevenALTV  48412  isubgredg  48631  upgrimwlklem5  48666  gricushgr  48682  stgrusgra  48724  isubgr3stgrlem8  48738  clintopval  48969  lmod0rng  48994  zlidlring  48999  2zrngagrp  49014  dmmpossx2  49117  zlmodzxzscm  49137  zlmodzxzadd  49138  domnmsuppn0  49149  rmsuppss  49150  scmsuppss  49151  ply1mulgsumlem4  49169  ldepsprlem  49252  lincresunit2  49258  nn0sumshdiglemB  49400  2arymptfv  49430  ackval42  49476  affinecomb1  49482  itschlc0yqe  49540  itsclquadb  49556  2itscp  49561  incat  50379  0setrec  50482