Theorem sylan9eqr 2786

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 2784	. 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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  sbcied2  3795  csbied2  3896  opthhausdorff0  5473  fun2ssres  6545  fcoi1  6716  fcoi2  6717  funssfv  6861  fvtp1  7151  nvof1o  7237  onuninsuci  7796  ot1stg  7961  ot2ndg  7962  el2xptp0  7994  mpomptsx  8022  dmmpossx  8024  fmpox  8025  2ndconst  8057  offsplitfpar  8075  mpoxopoveq  8175  rdgeq12  8358  rdgsucmptnf  8374  frsucmptn  8384  oev2  8464  oesuclem  8466  oawordeulem  8495  om00  8516  omass  8521  omeulem1  8523  oeoa  8538  oeoe  8540  nnmass  8565  oaabs2  8590  omabs  8592  mapsnend  8984  omxpenlem  9019  sbthlem4  9031  sbthlem6  9033  fodomr  9069  ssenen  9092  fodomfir  9255  fi0  9347  cantnfp1  9610  cnfcomlem  9628  ttrclselem2  9655  cardaleph  10018  cflim2  10192  axdc4lem  10384  fpwwe2lem11  10570  fpwwe2lem12  10571  rankcf  10706  inatsk  10707  ltrnq  10908  addclprlem1  10945  mulclprlem  10948  1idpr  10958  prlem936  10976  reclem3pr  10978  mulcmpblnrlem  10999  recexsrlem  11032  map2psrpr  11039  addid0  11573  subdivcomb2  11854  nnnn0addcl  12448  zindd  12611  qaddcl  12900  qmulcl  12902  qreccl  12904  xaddnemnf  13172  xaddnepnf  13173  xaddcom  13176  xnegdi  13184  xaddass  13185  xpncan  13187  xleadd1a  13189  xlt2add  13196  rexmul  13207  xmulgt0  13219  xmulge0  13220  xmulasslem3  13222  xlemul1a  13224  xadddilem  13230  xadddi2  13233  modmuladd  13854  modm1p1mod0  13863  modfzo0difsn  13884  seqf1olem2  13983  expp1  14009  expneg  14010  expcllem  14013  mulexp  14042  expmul  14048  sqoddm1div8  14184  bcpasc  14262  hashrabsn01  14314  fseq1hash  14317  hashinfxadd  14326  hashfzo  14370  fnfz0hash  14387  ffzo0hash  14390  hashf1lem1  14396  hashge2el2dif  14421  hash3tpexb  14435  hashdifsnp1  14447  lsw0  14506  ccatval1  14518  ccatval2  14519  swrdval  14584  ccatopth  14657  reuccatpfxs1  14688  splval  14692  repswswrd  14725  2cshwcshw  14767  s4dom  14861  wrdlen2i  14884  shftfn  15015  reim0b  15061  cjexp  15092  sqeqd  15108  fsumser  15672  sumsnf  15685  binomlem  15771  expcnv  15806  prodsn  15904  prodsnf  15906  bpolylem  15990  bpoly2  15999  bpoly3  16000  ef0lem  16020  dvdsnegb  16219  mod2eq1n2dvds  16293  m1expe  16320  m1expo  16321  m1exp1  16322  flodddiv4  16361  sadadd2lem2  16396  bezoutr1  16515  dvdslcm  16544  lcmeq0  16546  lcmcl  16547  lcmabs  16551  lcmgcdlem  16552  lcmdvds  16554  lcmf0val  16568  lcmftp  16582  lcmfunsnlem2  16586  mulgcddvds  16601  divgcdcoprmex  16612  pcge0  16809  pcadd  16836  pcmpt2  16840  prmreclem4  16866  ramval  16955  ramcl  16976  fvprmselelfz  16991  fvprmselgcd1  16992  ressid2  17180  ressval2  17181  mndind  18731  frmdval  18754  efmnd  18773  smndex1igid  18807  smndex1n0mnd  18815  mgm2nsgrplem3  18823  mulgfval  18977  mulgfvalALT  18978  mulgnn0subcl  18995  mulgnn0z  19009  cycsubm  19110  f1ghm0to0  19153  isga  19199  symgextfve  19325  symgfixf1  19343  f1omvdco2  19354  psgnsn  19426  odid  19444  gexid  19487  efgsval2  19639  frgpuptinv  19677  frgpup2  19682  dprdsn  19944  srgmulgass  20102  srgpcomp  20103  srgbinomlem4  20114  ringinvnzdiv  20186  rngcval  20503  ringcval  20532  isabvd  20697  issrng  20729  lmodvsmmulgdi  20779  mptscmfsupp0  20809  lvecinv  20999  lspdisj2  21013  lspfixed  21014  lspexch  21015  sralem  21059  srasca  21063  sravsca  21064  sraip  21065  znval  21421  psgndiflemB  21485  isphl  21513  assamulgscmlem2  21785  mplval  21874  opsrval  21929  psdmvr  22032  cply1mul  22159  gsummoncoe1  22171  evl1fval  22191  scmate  22373  scmatscm  22376  mdetdiagid  22463  mdetunilem7  22481  mdetuni0  22484  gsummatr01lem3  22520  gsummatr01lem4  22521  gsummatr01  22522  slesolinvbi  22544  cpmatacl  22579  cpmatinvcl  22580  pmatcollpw2lem  22640  monmatcollpw  22642  pmatcollpwfi  22645  mp2pm2mplem4  22672  pm2mp  22688  cpmadugsumlemF  22739  cpmadugsumfi  22740  cpmadumatpoly  22746  cayhamlem4  22751  cayleyhamilton0  22752  cayleyhamiltonALT  22754  indistopon  22864  0ntr  22934  pnrmopn  23206  reftr  23377  kgenval  23398  pt1hmeo  23669  fmval  23806  fmf  23808  istmd  23937  istgp  23940  tsmsval2  23993  isxmet2d  24191  xpsxmetlem  24243  xpsmet  24246  blfvalps  24247  tmsval  24345  isnlm  24539  nmoleub  24595  idnghm  24607  blssioo  24659  blcvx  24662  icccvx  24824  pcorevlem  24902  isclm  24940  caufval  25151  iscms  25221  mbfsup  25541  i1f1  25567  dvexp3  25858  rolle  25870  dvivth  25891  deg1add  25984  0dgr  26126  coefv0  26129  elqaalem2  26204  dvradcnv  26306  abelthlem8  26325  efper  26364  logtayl  26545  abscxpbnd  26639  relogbcxpb  26673  logbgcd1irr  26680  dcubic2  26730  rlimcnp2  26852  cvxcl  26871  zetacvg  26901  lgamgulmlem2  26916  vmaval  26999  chtub  27099  logexprlim  27112  dchrsum2  27155  sumdchr2  27157  bposlem2  27172  lgsdir  27219  lgsne0  27222  lgsdirnn0  27231  lgsdinn0  27232  lgsquadlem2  27268  2lgslem3a  27283  2lgslem3b  27284  2lgslem3c  27285  2lgslem3d  27286  2lgslem3a1  27287  2lgslem3b1  27288  2lgslem3c1  27289  2lgslem3d1  27290  2sqn0  27321  dchrvmasum2if  27384  dchrvmasumiflem1  27388  rpvmasum2  27399  pntpbnd1  27473  ostth2lem4  27523  expsp1  28291  trgcgrg  28418  tgcgr4  28434  ax5seglem1  28831  ax5seglem2  28832  ax5seglem5  28836  usgr1vr  29158  cplgr2vpr  29336  cplgr3v  29338  cusgrrusgr  29485  wlklenvm1  29525  wlk0prc  29556  wlksoneq1eq2  29566  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  crctcshwlkn0lem6  29718  crctcshlem4  29723  crctcsh  29727  wlkiswwlks1  29770  wwlksnext  29796  wwlksnextbi  29797  wwlksnextwrd  29800  midwwlks2s3  29855  clwlkclwwlklem2fv1  29897  clwlkclwwlklem2a4  29899  clwlkclwwlklem3  29903  clwwisshclwws  29917  erclwwlkeqlen  29921  clwwlkinwwlk  29942  clwwlkn2  29946  clwwlkf  29949  clwwlkf1  29951  eleclclwwlknlem2  29963  erclwwlkneqlen  29970  umgrhashecclwwlk  29980  eucrctshift  30145  eucrct2eupth  30147  fusgr2wsp2nb  30236  grpoidinvlem2  30407  vcz  30477  nvz  30571  lnon0  30700  ipasslem2  30734  htthlem  30819  hvpncan  30941  hiidge0  31000  normgt0  31029  hsn0elch  31150  shsel3  31217  spansneleq  31472  normcan  31478  h1datomi  31483  fh1  31520  spansncvi  31554  5oalem1  31556  5oalem3  31558  5oalem5  31560  3oalem2  31565  pjdsi  31614  kbpj  31858  0hmop  31885  0lnfn  31887  adj0  31896  nlelshi  31962  branmfn  32007  opsqrlem1  32042  hst1h  32129  mdsl0  32212  superpos  32256  sumdmdlem  32320  cdj3lem1  32336  f1od2  32617  xrpxdivcld  32828  xrge0npcan  32934  elrgspnlem2  33167  rlocf1  33197  resvid2  33275  resvval2  33276  qsdrng  33441  r1pquslmic  33549  rtelextdg2lem  33689  esumsnf  34027  esummulc1  34044  measxun2  34173  omsmeas  34287  sibfof  34304  probun  34383  signstfvn  34533  bnj517  34848  pthhashvtx  35088  ex-sategoelel  35381  mrsubfval  35468  msrval  35498  dfrdg2  35756  itgeq12i  36167  bj-prmoore  37076  bj-bary1lem1  37272  rdgeqoa  37331  finxpreclem2  37351  finxpreclem3  37354  matunitlindflem1  37583  poimirlem1  37588  poimirlem2  37589  poimirlem3  37590  poimirlem4  37591  poimirlem5  37592  poimirlem6  37593  poimirlem7  37594  poimirlem10  37597  poimirlem11  37598  poimirlem12  37599  poimirlem14  37601  poimirlem15  37602  poimirlem17  37604  poimirlem20  37607  poimirlem22  37609  poimirlem23  37610  poimirlem24  37611  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  mblfinlem2  37625  mblfinlem3  37626  ismblfin  37628  mbfposadd  37634  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  ftc1anclem8  37667  areacirc  37680  ismtyval  37767  ismrer1  37805  grposnOLD  37849  rabeq12f  38124  csbeq12  38125  iuneq12f  38130  lsatcv1  39014  glbconN  39343  glbconNOLD  39344  atltcvr  39402  3dim2  39435  islln2a  39484  2at0mat0  39492  islpln2a  39515  islvol2aN  39559  pmodlem2  39814  pmapjat1  39820  pcl0bN  39890  osumclN  39934  pexmidALTN  39945  lhp2at0nle  40002  4atexlemunv  40033  cdleme18b  40259  cdleme31sn1  40348  cdleme31sde  40352  cdleme31sn2  40356  ltrniotavalbN  40551  trljco  40707  cdlemh  40784  cdlemk40t  40885  cdlemk40f  40886  cdleml9  40951  dihmeetlem3N  41272  dochkrshp  41353  dihprrn  41393  dihjat1  41396  dvh3dim  41413  dochkrsm  41425  dochexmid  41435  lcfl7lem  41466  lcfl9a  41472  lclkrlem1  41473  mapdspex  41635  mapdindp2  41688  mapdh6dN  41706  hdmap1l6d  41780  hdmap11lem2  41809  hdmap14lem4a  41838  hdmapip0  41882  hlhilset  41901  nnadd1com  42228  mulgt0b2d  42439  fiabv  42497  prjspner1  42587  0prjspnrel  42588  jm2.26a  42962  onov0suclim  43236  oe0suclim  43239  cantnfresb  43286  onmcl  43293  omcl2  43295  tfsconcatun  43299  naddwordnexlem4  43363  mnringmulrcld  44190  radcnvrat  44276  sumsnd  44993  icccncfext  45858  fperdvper  45890  dvcosax  45897  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  volioc  45943  itgiccshift  45951  stoweidlem34  46005  dirkercncflem2  46075  fourierdlem32  46110  fourierdlem41  46119  fourierdlem48  46125  fourierdlem64  46141  fourierdlem73  46150  fourierdlem79  46156  fourierdlem82  46159  fourierdlem97  46174  fourierdlem101  46178  fourierdlem109  46186  fourierdlem111  46188  fouriersw  46202  elaa2  46205  etransclem24  46229  etransclem25  46230  etransclem46  46251  nnfoctbdjlem  46426  ismeannd  46438  smfpimltxr  46718  smfpimgtxr  46751  ndfatafv2undef  47186  fzopredsuc  47297  m1modmmod  47332  modlt0b  47337  prproropf1olem3  47479  prproropf1olem4  47480  fmtnorec2lem  47516  2pwp1prmfmtno  47564  sfprmdvdsmersenne  47577  sgprmdvdsmersenne  47578  lighneallem2  47580  lighneallem3  47581  dfodd6  47611  dfeven4  47612  m1expevenALTV  47621  isubgredg  47839  upgrimwlklem5  47874  gricushgr  47890  stgrusgra  47931  isubgr3stgrlem8  47945  clintopval  48165  lmod0rng  48190  zlidlring  48195  2zrngagrp  48210  dmmpossx2  48298  zlmodzxzscm  48318  zlmodzxzadd  48319  domnmsuppn0  48330  rmsuppss  48331  scmsuppss  48332  ply1mulgsumlem4  48351  ldepsprlem  48434  lincresunit2  48440  nn0sumshdiglemB  48582  2arymptfv  48612  ackval42  48658  affinecomb1  48664  itschlc0yqe  48722  itsclquadb  48738  2itscp  48743  incat  49563  0setrec  49666