Theorem sylan9eqr 2799

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 2797	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	3	ancoms 458	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  sbcied2  3833  csbied2  3936  opthhausdorff0  5523  fun2ssres  6611  fcoi1  6782  fcoi2  6783  funssfv  6927  fvtp1  7215  nvof1o  7300  onuninsuci  7861  ot1stg  8028  ot2ndg  8029  el2xptp0  8061  mpomptsx  8089  dmmpossx  8091  fmpox  8092  2ndconst  8126  offsplitfpar  8144  mpoxopoveq  8244  wfrlem10OLD  8358  rdgeq12  8453  rdgsucmptnf  8469  frsucmptn  8479  oev2  8561  oesuclem  8563  oawordeulem  8592  om00  8613  omass  8618  omeulem1  8620  oeoa  8635  oeoe  8637  nnmass  8662  oaabs2  8687  omabs  8689  mapsnend  9076  omxpenlem  9113  sbthlem4  9126  sbthlem6  9128  fodomr  9168  ssenen  9191  fodomfir  9368  fi0  9460  cantnfp1  9721  cnfcomlem  9739  ttrclselem2  9766  cardaleph  10129  cflim2  10303  axdc4lem  10495  fpwwe2lem11  10681  fpwwe2lem12  10682  rankcf  10817  inatsk  10818  ltrnq  11019  addclprlem1  11056  mulclprlem  11059  1idpr  11069  prlem936  11087  reclem3pr  11089  mulcmpblnrlem  11110  recexsrlem  11143  map2psrpr  11150  addid0  11682  subdivcomb2  11963  nnnn0addcl  12556  zindd  12719  qaddcl  13007  qmulcl  13009  qreccl  13011  xaddnemnf  13278  xaddnepnf  13279  xaddcom  13282  xnegdi  13290  xaddass  13291  xpncan  13293  xleadd1a  13295  xlt2add  13302  rexmul  13313  xmulgt0  13325  xmulge0  13326  xmulasslem3  13328  xlemul1a  13330  xadddilem  13336  xadddi2  13339  modmuladd  13954  modm1p1mod0  13963  modfzo0difsn  13984  seqf1olem2  14083  expp1  14109  expneg  14110  expcllem  14113  mulexp  14142  expmul  14148  sqoddm1div8  14282  bcpasc  14360  hashrabsn01  14412  fseq1hash  14415  hashinfxadd  14424  hashfzo  14468  fnfz0hash  14485  ffzo0hash  14488  hashf1lem1  14494  hashge2el2dif  14519  hash3tpexb  14533  hashdifsnp1  14545  lsw0  14603  ccatval1  14615  ccatval2  14616  swrdval  14681  ccatopth  14754  reuccatpfxs1  14785  splval  14789  repswswrd  14822  2cshwcshw  14864  s4dom  14958  wrdlen2i  14981  shftfn  15112  reim0b  15158  cjexp  15189  sqeqd  15205  fsumser  15766  sumsnf  15779  binomlem  15865  expcnv  15900  prodsn  15998  prodsnf  16000  bpolylem  16084  bpoly2  16093  bpoly3  16094  ef0lem  16114  dvdsnegb  16311  mod2eq1n2dvds  16384  m1expe  16411  m1expo  16412  m1exp1  16413  flodddiv4  16452  sadadd2lem2  16487  bezoutr1  16606  dvdslcm  16635  lcmeq0  16637  lcmcl  16638  lcmabs  16642  lcmgcdlem  16643  lcmdvds  16645  lcmf0val  16659  lcmftp  16673  lcmfunsnlem2  16677  mulgcddvds  16692  divgcdcoprmex  16703  pcge0  16900  pcadd  16927  pcmpt2  16931  prmreclem4  16957  ramval  17046  ramcl  17067  fvprmselelfz  17082  fvprmselgcd1  17083  ressid2  17278  ressval2  17279  mndind  18841  frmdval  18864  efmnd  18883  smndex1igid  18917  smndex1n0mnd  18925  mgm2nsgrplem3  18933  mulgfval  19087  mulgfvalALT  19088  mulgnn0subcl  19105  mulgnn0z  19119  cycsubm  19220  f1ghm0to0  19263  isga  19309  symgextfve  19437  symgfixf1  19455  f1omvdco2  19466  psgnsn  19538  odid  19556  gexid  19599  efgsval2  19751  frgpuptinv  19789  frgpup2  19794  dprdsn  20056  srgmulgass  20214  srgpcomp  20215  srgbinomlem4  20226  ringinvnzdiv  20298  rngcval  20618  ringcval  20647  isabvd  20813  issrng  20845  lmodvsmmulgdi  20895  mptscmfsupp0  20925  lvecinv  21115  lspdisj2  21129  lspfixed  21130  lspexch  21131  sralem  21175  sralemOLD  21176  srasca  21183  srascaOLD  21184  sravsca  21185  sravscaOLD  21186  sraip  21187  znval  21550  psgndiflemB  21618  isphl  21646  assamulgscmlem2  21920  mplval  22009  opsrval  22064  psdmvr  22173  cply1mul  22300  gsummoncoe1  22312  evl1fval  22332  scmate  22516  scmatscm  22519  mdetdiagid  22606  mdetunilem7  22624  mdetuni0  22627  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  slesolinvbi  22687  cpmatacl  22722  cpmatinvcl  22723  pmatcollpw2lem  22783  monmatcollpw  22785  pmatcollpwfi  22788  mp2pm2mplem4  22815  pm2mp  22831  cpmadugsumlemF  22882  cpmadugsumfi  22883  cpmadumatpoly  22889  cayhamlem4  22894  cayleyhamilton0  22895  cayleyhamiltonALT  22897  indistopon  23008  0ntr  23079  pnrmopn  23351  reftr  23522  kgenval  23543  pt1hmeo  23814  fmval  23951  fmf  23953  istmd  24082  istgp  24085  tsmsval2  24138  isxmet2d  24337  xpsxmetlem  24389  xpsmet  24392  blfvalps  24393  tmsval  24493  isnlm  24696  nmoleub  24752  idnghm  24764  blssioo  24816  blcvx  24819  icccvx  24981  pcorevlem  25059  isclm  25097  caufval  25309  iscms  25379  mbfsup  25699  i1f1  25725  dvexp3  26016  rolle  26028  dvivth  26049  deg1add  26142  0dgr  26284  coefv0  26287  elqaalem2  26362  dvradcnv  26464  abelthlem8  26483  efper  26521  logtayl  26702  abscxpbnd  26796  relogbcxpb  26830  logbgcd1irr  26837  dcubic2  26887  rlimcnp2  27009  cvxcl  27028  zetacvg  27058  lgamgulmlem2  27073  vmaval  27156  chtub  27256  logexprlim  27269  dchrsum2  27312  sumdchr2  27314  bposlem2  27329  lgsdir  27376  lgsne0  27379  lgsdirnn0  27388  lgsdinn0  27389  lgsquadlem2  27425  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgslem3d1  27447  2sqn0  27478  dchrvmasum2if  27541  dchrvmasumiflem1  27545  rpvmasum2  27556  pntpbnd1  27630  ostth2lem4  27680  expsp1  28412  trgcgrg  28523  tgcgr4  28539  ax5seglem1  28943  ax5seglem2  28944  ax5seglem5  28948  usgr1vr  29272  cplgr2vpr  29450  cplgr3v  29452  cusgrrusgr  29599  wlklenvm1  29640  wlk0prc  29672  wlksoneq1eq2  29682  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  crctcshlem4  29840  crctcsh  29844  wlkiswwlks1  29887  wwlksnext  29913  wwlksnextbi  29914  wwlksnextwrd  29917  midwwlks2s3  29972  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2a4  30016  clwlkclwwlklem3  30020  clwwisshclwws  30034  erclwwlkeqlen  30038  clwwlkinwwlk  30059  clwwlkn2  30063  clwwlkf  30066  clwwlkf1  30068  eleclclwwlknlem2  30080  erclwwlkneqlen  30087  umgrhashecclwwlk  30097  eucrctshift  30262  eucrct2eupth  30264  fusgr2wsp2nb  30353  grpoidinvlem2  30524  vcz  30594  nvz  30688  lnon0  30817  ipasslem2  30851  htthlem  30936  hvpncan  31058  hiidge0  31117  normgt0  31146  hsn0elch  31267  shsel3  31334  spansneleq  31589  normcan  31595  h1datomi  31600  fh1  31637  spansncvi  31671  5oalem1  31673  5oalem3  31675  5oalem5  31677  3oalem2  31682  pjdsi  31731  kbpj  31975  0hmop  32002  0lnfn  32004  adj0  32013  nlelshi  32079  branmfn  32124  opsqrlem1  32159  hst1h  32246  mdsl0  32329  superpos  32373  sumdmdlem  32437  cdj3lem1  32453  f1od2  32732  xrpxdivcld  32917  xrge0npcan  33025  elrgspnlem2  33247  rlocf1  33277  resvid2  33354  resvval2  33355  qsdrng  33525  r1pquslmic  33631  rtelextdg2lem  33767  esumsnf  34065  esummulc1  34082  measxun2  34211  omsmeas  34325  sibfof  34342  probun  34421  signstfvn  34584  bnj517  34899  pthhashvtx  35133  ex-sategoelel  35426  mrsubfval  35513  msrval  35543  dfrdg2  35796  itgeq12i  36207  bj-prmoore  37116  bj-bary1lem1  37312  rdgeqoa  37371  finxpreclem2  37391  finxpreclem3  37394  matunitlindflem1  37623  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem14  37641  poimirlem15  37642  poimirlem17  37644  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  mblfinlem2  37665  mblfinlem3  37666  ismblfin  37668  mbfposadd  37674  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  ftc1anclem8  37707  areacirc  37720  ismtyval  37807  ismrer1  37845  grposnOLD  37889  rabeq12f  38164  csbeq12  38165  iuneq12f  38170  lsatcv1  39049  glbconN  39378  glbconNOLD  39379  atltcvr  39437  3dim2  39470  islln2a  39519  2at0mat0  39527  islpln2a  39550  islvol2aN  39594  pmodlem2  39849  pmapjat1  39855  pcl0bN  39925  osumclN  39969  pexmidALTN  39980  lhp2at0nle  40037  4atexlemunv  40068  cdleme18b  40294  cdleme31sn1  40383  cdleme31sde  40387  cdleme31sn2  40391  ltrniotavalbN  40586  trljco  40742  cdlemh  40819  cdlemk40t  40920  cdlemk40f  40921  cdleml9  40986  dihmeetlem3N  41307  dochkrshp  41388  dihprrn  41428  dihjat1  41431  dvh3dim  41448  dochkrsm  41460  dochexmid  41470  lcfl7lem  41501  lcfl9a  41507  lclkrlem1  41508  mapdspex  41670  mapdindp2  41723  mapdh6dN  41741  hdmap1l6d  41815  hdmap11lem2  41844  hdmap14lem4a  41873  hdmapip0  41917  hlhilset  41936  nnadd1com  42302  fiabv  42546  prjspner1  42636  0prjspnrel  42637  jm2.26a  43012  onov0suclim  43287  oe0suclim  43290  cantnfresb  43337  onmcl  43344  omcl2  43346  tfsconcatun  43350  naddwordnexlem4  43414  mnringmulrcld  44247  radcnvrat  44333  sumsnd  45031  icccncfext  45902  fperdvper  45934  dvcosax  45941  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  volioc  45987  itgiccshift  45995  stoweidlem34  46049  dirkercncflem2  46119  fourierdlem32  46154  fourierdlem41  46163  fourierdlem48  46169  fourierdlem64  46185  fourierdlem73  46194  fourierdlem79  46200  fourierdlem82  46203  fourierdlem97  46218  fourierdlem101  46222  fourierdlem109  46230  fourierdlem111  46232  fouriersw  46246  elaa2  46249  etransclem24  46273  etransclem25  46274  etransclem46  46295  nnfoctbdjlem  46470  ismeannd  46482  smfpimltxr  46762  smfpimgtxr  46795  ndfatafv2undef  47224  fzopredsuc  47335  prproropf1olem3  47492  prproropf1olem4  47493  fmtnorec2lem  47529  2pwp1prmfmtno  47577  sfprmdvdsmersenne  47590  sgprmdvdsmersenne  47591  lighneallem2  47593  lighneallem3  47594  dfodd6  47624  dfeven4  47625  m1expevenALTV  47634  isubgredg  47852  gricushgr  47886  stgrusgra  47926  isubgr3stgrlem8  47940  clintopval  48120  lmod0rng  48145  zlidlring  48150  2zrngagrp  48165  dmmpossx2  48253  zlmodzxzscm  48273  zlmodzxzadd  48274  domnmsuppn0  48285  rmsuppss  48286  scmsuppss  48287  ply1mulgsumlem4  48306  ldepsprlem  48389  lincresunit2  48395  m1modmmod  48442  nn0sumshdiglemB  48541  2arymptfv  48571  ackval42  48617  affinecomb1  48623  itschlc0yqe  48681  itsclquadb  48697  2itscp  48702  0setrec  49223