Theorem sylan9eqr 2793

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  sbcied2  3785  csbied2  3886  opthhausdorff0  5466  fun2ssres  6537  fcoi1  6708  fcoi2  6709  funssfv  6855  fvtp1  7141  nvof1o  7226  onuninsuci  7782  ot1stg  7947  ot2ndg  7948  el2xptp0  7980  mpomptsx  8008  dmmpossx  8010  fmpox  8011  2ndconst  8043  offsplitfpar  8061  mpoxopoveq  8161  rdgeq12  8344  rdgsucmptnf  8360  frsucmptn  8370  oev2  8450  oesuclem  8452  oawordeulem  8481  om00  8502  omass  8507  omeulem1  8509  oeoa  8525  oeoe  8527  nnmass  8552  oaabs2  8577  omabs  8579  mapsnend  8973  omxpenlem  9006  sbthlem4  9018  sbthlem6  9020  fodomr  9056  ssenen  9079  fodomfir  9228  fi0  9323  cantnfp1  9590  cnfcomlem  9608  ttrclselem2  9635  cardaleph  9999  cflim2  10173  axdc4lem  10365  fpwwe2lem11  10552  fpwwe2lem12  10553  rankcf  10688  inatsk  10689  ltrnq  10890  addclprlem1  10927  mulclprlem  10930  1idpr  10940  prlem936  10958  reclem3pr  10960  mulcmpblnrlem  10981  recexsrlem  11014  map2psrpr  11021  addid0  11556  subdivcomb2  11837  nnnn0addcl  12431  zindd  12593  qaddcl  12878  qmulcl  12880  qreccl  12882  xaddnemnf  13151  xaddnepnf  13152  xaddcom  13155  xnegdi  13163  xaddass  13164  xpncan  13166  xleadd1a  13168  xlt2add  13175  rexmul  13186  xmulgt0  13198  xmulge0  13199  xmulasslem3  13201  xlemul1a  13203  xadddilem  13209  xadddi2  13212  modmuladd  13836  modm1p1mod0  13845  modfzo0difsn  13866  seqf1olem2  13965  expp1  13991  expneg  13992  expcllem  13995  mulexp  14024  expmul  14030  sqoddm1div8  14166  bcpasc  14244  hashrabsn01  14296  fseq1hash  14299  hashinfxadd  14308  hashfzo  14352  fnfz0hash  14369  ffzo0hash  14372  hashf1lem1  14378  hashge2el2dif  14403  hash3tpexb  14417  hashdifsnp1  14429  lsw0  14488  ccatval1  14500  ccatval2  14501  swrdval  14567  ccatopth  14639  reuccatpfxs1  14670  splval  14674  repswswrd  14707  2cshwcshw  14748  s4dom  14842  wrdlen2i  14865  shftfn  14996  reim0b  15042  cjexp  15073  sqeqd  15089  fsumser  15653  sumsnf  15666  binomlem  15752  expcnv  15787  prodsn  15885  prodsnf  15887  bpolylem  15971  bpoly2  15980  bpoly3  15981  ef0lem  16001  dvdsnegb  16200  mod2eq1n2dvds  16274  m1expe  16301  m1expo  16302  m1exp1  16303  flodddiv4  16342  sadadd2lem2  16377  bezoutr1  16496  dvdslcm  16525  lcmeq0  16527  lcmcl  16528  lcmabs  16532  lcmgcdlem  16533  lcmdvds  16535  lcmf0val  16549  lcmftp  16563  lcmfunsnlem2  16567  mulgcddvds  16582  divgcdcoprmex  16593  pcge0  16790  pcadd  16817  pcmpt2  16821  prmreclem4  16847  ramval  16936  ramcl  16957  fvprmselelfz  16972  fvprmselgcd1  16973  ressid2  17161  ressval2  17162  mndind  18753  frmdval  18776  efmnd  18795  smndex1igid  18829  smndex1n0mnd  18837  mgm2nsgrplem3  18845  mulgfval  18999  mulgfvalALT  19000  mulgnn0subcl  19017  mulgnn0z  19031  cycsubm  19131  f1ghm0to0  19174  isga  19220  symgextfve  19348  symgfixf1  19366  f1omvdco2  19377  psgnsn  19449  odid  19467  gexid  19510  efgsval2  19662  frgpuptinv  19700  frgpup2  19705  dprdsn  19967  srgmulgass  20152  srgpcomp  20153  srgbinomlem4  20164  ringinvnzdiv  20236  rngcval  20551  ringcval  20580  isabvd  20745  issrng  20777  lmodvsmmulgdi  20848  mptscmfsupp0  20878  lvecinv  21068  lspdisj2  21082  lspfixed  21083  lspexch  21084  sralem  21128  srasca  21132  sravsca  21133  sraip  21134  znval  21490  psgndiflemB  21555  isphl  21583  assamulgscmlem2  21856  mplval  21944  opsrval  22001  psdmvr  22112  cply1mul  22240  gsummoncoe1  22252  evl1fval  22272  scmate  22454  scmatscm  22457  mdetdiagid  22544  mdetunilem7  22562  mdetuni0  22565  gsummatr01lem3  22601  gsummatr01lem4  22602  gsummatr01  22603  slesolinvbi  22625  cpmatacl  22660  cpmatinvcl  22661  pmatcollpw2lem  22721  monmatcollpw  22723  pmatcollpwfi  22726  mp2pm2mplem4  22753  pm2mp  22769  cpmadugsumlemF  22820  cpmadugsumfi  22821  cpmadumatpoly  22827  cayhamlem4  22832  cayleyhamilton0  22833  cayleyhamiltonALT  22835  indistopon  22945  0ntr  23015  pnrmopn  23287  reftr  23458  kgenval  23479  pt1hmeo  23750  fmval  23887  fmf  23889  istmd  24018  istgp  24021  tsmsval2  24074  isxmet2d  24271  xpsxmetlem  24323  xpsmet  24326  blfvalps  24327  tmsval  24425  isnlm  24619  nmoleub  24675  idnghm  24687  blssioo  24739  blcvx  24742  icccvx  24904  pcorevlem  24982  isclm  25020  caufval  25231  iscms  25301  mbfsup  25621  i1f1  25647  dvexp3  25938  rolle  25950  dvivth  25971  deg1add  26064  0dgr  26206  coefv0  26209  elqaalem2  26284  dvradcnv  26386  abelthlem8  26405  efper  26444  logtayl  26625  abscxpbnd  26719  relogbcxpb  26753  logbgcd1irr  26760  dcubic2  26810  rlimcnp2  26932  cvxcl  26951  zetacvg  26981  lgamgulmlem2  26996  vmaval  27079  chtub  27179  logexprlim  27192  dchrsum2  27235  sumdchr2  27237  bposlem2  27252  lgsdir  27299  lgsne0  27302  lgsdirnn0  27311  lgsdinn0  27312  lgsquadlem2  27348  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2sqn0  27401  dchrvmasum2if  27464  dchrvmasumiflem1  27468  rpvmasum2  27479  pntpbnd1  27553  ostth2lem4  27603  expsp1  28425  trgcgrg  28587  tgcgr4  28603  ax5seglem1  29001  ax5seglem2  29002  ax5seglem5  29006  usgr1vr  29328  cplgr2vpr  29506  cplgr3v  29508  cusgrrusgr  29655  wlklenvm1  29695  wlk0prc  29726  wlksoneq1eq2  29736  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  crctcshlem4  29893  crctcsh  29897  wlkiswwlks1  29940  wwlksnext  29966  wwlksnextbi  29967  wwlksnextwrd  29970  midwwlks2s3  30025  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2a4  30072  clwlkclwwlklem3  30076  clwwisshclwws  30090  erclwwlkeqlen  30094  clwwlkinwwlk  30115  clwwlkn2  30119  clwwlkf  30122  clwwlkf1  30124  eleclclwwlknlem2  30136  erclwwlkneqlen  30143  umgrhashecclwwlk  30153  eucrctshift  30318  eucrct2eupth  30320  fusgr2wsp2nb  30409  grpoidinvlem2  30580  vcz  30650  nvz  30744  lnon0  30873  ipasslem2  30907  htthlem  30992  hvpncan  31114  hiidge0  31173  normgt0  31202  hsn0elch  31323  shsel3  31390  spansneleq  31645  normcan  31651  h1datomi  31656  fh1  31693  spansncvi  31727  5oalem1  31729  5oalem3  31731  5oalem5  31733  3oalem2  31738  pjdsi  31787  kbpj  32031  0hmop  32058  0lnfn  32060  adj0  32069  nlelshi  32135  branmfn  32180  opsqrlem1  32215  hst1h  32302  mdsl0  32385  superpos  32429  sumdmdlem  32493  cdj3lem1  32509  f1od2  32798  xrpxdivcld  33016  xrge0npcan  33102  elrgspnlem2  33325  rlocf1  33355  resvid2  33411  resvval2  33412  qsdrng  33578  r1pquslmic  33692  mplvrpmmhm  33711  mplvrpmrhm  33712  esplyfval0  33722  vietalem  33735  rtelextdg2lem  33883  esumsnf  34221  esummulc1  34238  measxun2  34367  omsmeas  34480  sibfof  34497  probun  34576  signstfvn  34726  bnj517  35041  pthhashvtx  35322  ex-sategoelel  35615  mrsubfval  35702  msrval  35732  dfrdg2  35987  itgeq12i  36400  bj-prmoore  37320  bj-bary1lem1  37516  rdgeqoa  37575  finxpreclem2  37595  finxpreclem3  37598  matunitlindflem1  37817  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem14  37835  poimirlem15  37836  poimirlem17  37838  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  mblfinlem2  37859  mblfinlem3  37860  ismblfin  37862  mbfposadd  37868  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  ftc1anclem8  37901  areacirc  37914  ismtyval  38001  ismrer1  38039  grposnOLD  38083  rabeq12f  38358  csbeq12  38359  iuneq12f  38364  lsatcv1  39308  glbconN  39637  atltcvr  39695  3dim2  39728  islln2a  39777  2at0mat0  39785  islpln2a  39808  islvol2aN  39852  pmodlem2  40107  pmapjat1  40113  pcl0bN  40183  osumclN  40227  pexmidALTN  40238  lhp2at0nle  40295  4atexlemunv  40326  cdleme18b  40552  cdleme31sn1  40641  cdleme31sde  40645  cdleme31sn2  40649  ltrniotavalbN  40844  trljco  41000  cdlemh  41077  cdlemk40t  41178  cdlemk40f  41179  cdleml9  41244  dihmeetlem3N  41565  dochkrshp  41646  dihprrn  41686  dihjat1  41689  dvh3dim  41706  dochkrsm  41718  dochexmid  41728  lcfl7lem  41759  lcfl9a  41765  lclkrlem1  41766  mapdspex  41928  mapdindp2  41981  mapdh6dN  41999  hdmap1l6d  42073  hdmap11lem2  42102  hdmap14lem4a  42131  hdmapip0  42175  hlhilset  42194  nnadd1com  42522  mulgt0b2d  42733  fiabv  42791  prjspner1  42869  0prjspnrel  42870  jm2.26a  43242  onov0suclim  43516  oe0suclim  43519  cantnfresb  43566  onmcl  43573  omcl2  43575  tfsconcatun  43579  naddwordnexlem4  43643  mnringmulrcld  44469  radcnvrat  44555  sumsnd  45271  icccncfext  46131  fperdvper  46163  dvcosax  46170  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  volioc  46216  itgiccshift  46224  stoweidlem34  46278  dirkercncflem2  46348  fourierdlem32  46383  fourierdlem41  46392  fourierdlem48  46398  fourierdlem64  46414  fourierdlem73  46423  fourierdlem79  46429  fourierdlem82  46432  fourierdlem97  46447  fourierdlem101  46451  fourierdlem109  46459  fourierdlem111  46461  fouriersw  46475  elaa2  46478  etransclem24  46502  etransclem25  46503  etransclem46  46524  nnfoctbdjlem  46699  ismeannd  46711  smfpimltxr  46991  smfpimgtxr  47024  ndfatafv2undef  47458  fzopredsuc  47569  m1modmmod  47604  modlt0b  47609  prproropf1olem3  47751  prproropf1olem4  47752  fmtnorec2lem  47788  2pwp1prmfmtno  47836  sfprmdvdsmersenne  47849  sgprmdvdsmersenne  47850  lighneallem2  47852  lighneallem3  47853  dfodd6  47883  dfeven4  47884  m1expevenALTV  47893  isubgredg  48112  upgrimwlklem5  48147  gricushgr  48163  stgrusgra  48205  isubgr3stgrlem8  48219  clintopval  48450  lmod0rng  48475  zlidlring  48480  2zrngagrp  48495  dmmpossx2  48583  zlmodzxzscm  48603  zlmodzxzadd  48604  domnmsuppn0  48615  rmsuppss  48616  scmsuppss  48617  ply1mulgsumlem4  48635  ldepsprlem  48718  lincresunit2  48724  nn0sumshdiglemB  48866  2arymptfv  48896  ackval42  48942  affinecomb1  48948  itschlc0yqe  49006  itsclquadb  49022  2itscp  49027  incat  49846  0setrec  49949