Theorem sylan9eqr 2818

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  sbcied2  3783  csbied2  3884  opthhausdorff0  5491  fun2ssres  6583  fcoi1  6754  fcoi2  6755  funssfv  6904  fvtp1  7198  nvof1o  7286  onuninsuci  7849  ot1stg  8013  ot2ndg  8014  el2xptp0  8045  mpomptsx  8073  dmmpossx  8075  fmpox  8076  2ndconst  8110  offsplitfpar  8128  mpoxopoveq  8229  rdgeq12  8414  rdgsucmptnf  8430  frsucmptn  8440  oev2  8524  oesuclem  8526  oawordeulem  8555  om00  8576  omass  8581  omeulem1  8583  oeoa  8599  oeoe  8601  nnmass  8626  oaabs2  8651  omabs  8653  mapsnend  9057  omxpenlem  9090  sbthlem4  9102  sbthlem6  9104  fodomr  9140  ssenen  9163  fodomfir  9312  fi0  9405  cantnfp1  9675  cnfcomlem  9693  ttrclselem2  9720  cardaleph  10161  cflim2  10334  axdc4lem  10526  fpwwe2lem11  10719  fpwwe2lem12  10720  rankcf  10855  inatsk  10856  ltrnq  11057  addclprlem1  11094  mulclprlem  11097  1idpr  11107  prlem936  11125  reclem3pr  11127  mulcmpblnrlem  11148  recexsrlem  11181  map2psrpr  11188  addid0  11728  subdivcomb2  12006  nnadd1com  12354  nnnn0addcl  12629  zindd  12793  qaddcl  13086  qmulcl  13088  qreccl  13090  xaddnemnf  13359  xaddnepnf  13360  xaddcom  13363  xnegdi  13371  xaddass  13372  xpncan  13374  xleadd1a  13376  xlt2add  13383  rexmul  13394  xmulgt0  13406  xmulge0  13407  xmulasslem3  13409  xlemul1a  13411  xadddilem  13417  xadddi2  13420  modmuladd  14049  modm1p1mod0  14058  modfzo0difsn  14079  seqf1olem2  14178  expp1  14204  expneg  14205  expcllem  14208  mulexp  14237  expmul  14243  sqoddm1div8  14380  bcpasc  14458  hashrabsn01  14510  fseq1hash  14513  hashinfxadd  14522  hashfzo  14567  fnfz0hash  14584  ffzo0hash  14587  hashf1lem1  14593  hashge2el2dif  14618  hash3tpexb  14632  hashdifsnp1  14644  lsw0  14703  ccatval1  14715  ccatval2  14716  swrdval  14784  ccatopth  14858  reuccatpfxs1  14889  splval  14893  repswswrd  14928  2cshwcshw  14969  s4dom  15063  wrdlen2i  15086  shftfn  15219  reim0b  15279  cjexp  15310  sqeqd  15326  fsumser  15889  sumsnf  15902  binomlem  15991  expcnv  16026  prodsn  16122  prodsnf  16124  bpolylem  16207  bpoly2  16216  bpoly3  16217  ef0lem  16237  dvdsnegb  16436  mod2eq1n2dvds  16510  m1expe  16537  m1expo  16538  m1exp1  16539  flodddiv4  16578  sadadd2lem2  16613  bezoutr1  16737  dvdslcm  16766  lcmeq0  16768  lcmcl  16769  lcmabs  16773  lcmgcdlem  16774  lcmdvds  16776  lcmf0val  16790  lcmftp  16804  lcmfunsnlem2  16808  mulgcddvds  16823  divgcdcoprmex  16834  pcge0  17033  pcadd  17060  pcmpt2  17064  prmreclem4  17090  ramval  17179  ramcl  17200  fvprmselelfz  17215  fvprmselgcd1  17216  ressid2  17405  ressval2  17406  mndind  19017  frmdval  19040  efmnd  19059  smndex1igid  19095  smndex1igidOLD  19096  smndex1n0mnd  19104  mgm2nsgrplem3  19112  mulgfval  19272  mulgfvalALT  19273  mulgnn0subcl  19290  mulgnn0z  19304  cycsubm  19410  f1ghm0to0  19452  isga  19498  symgextfve  19626  symgfixf1  19644  f1omvdco2  19655  psgnsn  19727  odid  19745  gexid  19788  efgsval2  19940  frgpuptinv  19978  frgpup2  19983  dprdsn  20245  srgmulgass  20436  srgpcomp  20437  srgbinomlem4  20448  ringinvnzdiv  20525  rngcval  20863  ringcval  20892  isabvd  21062  issrng  21094  lmodvsmmulgdi  21165  mptscmfsupp0  21195  lvecinv  21384  lspdisj2  21398  lspfixed  21399  lspexch  21400  sralem  21444  srasca  21448  sravsca  21449  sraip  21450  znval  21834  psgndiflemB  21899  isphl  21927  assamulgscmlem2  22201  mplval  22289  opsrval  22348  psdmvr  22483  cply1mul  22607  gsummoncoe1  22619  evl1fval  22639  scmate  22818  scmatscm  22821  mdetdiagid  22908  mdetunilem7  22926  mdetuni0  22929  gsummatr01lem3  22965  gsummatr01lem4  22966  gsummatr01  22967  matunitlindflem1  22987  slesolinvbi  22992  cpmatacl  23027  cpmatinvcl  23028  pmatcollpw2lem  23088  monmatcollpw  23090  pmatcollpwfi  23093  mp2pm2mplem4  23120  pm2mp  23136  cpmadugsumlemF  23187  cpmadugsumfi  23188  cpmadumatpoly  23194  cayhamlem4  23199  cayleyhamilton0  23200  cayleyhamiltonALT  23202  indistopon  23312  0ntr  23382  pnrmopn  23654  reftr  23826  kgenval  23847  pt1hmeo  24118  fmval  24255  fmf  24257  istmd  24386  istgp  24389  tsmsval2  24442  isxmet2d  24639  xpsxmetlem  24691  xpsmet  24694  blfvalps  24695  tmsval  24793  isnlm  24987  nmoleub  25043  idnghm  25055  blssioo  25107  blcvx  25110  icccvx  25264  pcorevlem  25340  isclm  25378  caufval  25589  iscms  25659  mbfsup  25978  i1f1  26004  dvexp3  26291  rolle  26303  dvivth  26323  deg1add  26414  0dgr  26557  coefv0  26560  elqaalem2  26636  dvradcnv  26741  abelthlem8  26759  efper  26801  logtayl  26981  abscxpbnd  27074  relogbcxpb  27108  logbgcd1irr  27115  dcubic2  27165  rlimcnp2  27287  cvxcl  27305  zetacvg  27335  lgamgulmlem2  27350  vmaval  27433  chtub  27532  logexprlim  27545  dchrsum2  27588  sumdchr2  27590  bposlem2  27605  lgsdir  27652  lgsne0  27655  lgsdirnn0  27664  lgsdinn0  27665  lgsquadlem2  27701  2lgslem3a  27716  2lgslem3b  27717  2lgslem3c  27718  2lgslem3d  27719  2lgslem3a1  27720  2lgslem3b1  27721  2lgslem3c1  27722  2lgslem3d1  27723  2sqn0  27754  dchrvmasum2if  27817  dchrvmasumiflem1  27821  rpvmasum2  27832  pntpbnd1  27906  ostth2lem4  27956  expsp1  28808  trgcgrg  28971  tgcgr4  28987  ax5seglem1  29499  ax5seglem2  29500  ax5seglem5  29504  usgr1vr  29829  cplgr2vpr  30007  cplgr3v  30009  cusgrrusgr  30155  wlklenvm1  30195  wlk0prc  30226  wlksoneq1eq2  30236  pthhashvtx  30308  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  crctcshwlkn0lem6  30397  crctcshlem4  30402  crctcsh  30406  wlkiswwlks1  30449  wwlksnext  30475  wwlksnextbi  30476  wwlksnextwrd  30479  midwwlks2s3  30534  clwlkclwwlklem2fv1  30579  clwlkclwwlklem2a4  30581  clwlkclwwlklem3  30585  clwwisshclwws  30599  erclwwlkeqlen  30603  clwwlkinwwlk  30624  clwwlkn2  30628  clwwlkf  30631  clwwlkf1  30633  eleclclwwlknlem2  30645  erclwwlkneqlen  30652  umgrhashecclwwlk  30662  eucrctshift  30837  eucrct2eupth  30839  fusgr2wsp2nb  30928  grpoidinvlem2  31100  vcz  31170  nvz  31264  lnon0  31393  ipasslem2  31427  htthlem  31512  hvpncan  31634  hiidge0  31693  normgt0  31722  hsn0elch  31843  shsel3  31910  spansneleq  32165  normcan  32171  h1datomi  32176  fh1  32213  spansncvi  32247  5oalem1  32249  5oalem3  32251  5oalem5  32253  3oalem2  32258  pjdsi  32307  kbpj  32551  0hmop  32578  0lnfn  32580  adj0  32589  nlelshi  32655  branmfn  32700  opsqrlem1  32735  hst1h  32822  mdsl0  32905  superpos  32949  sumdmdlem  33013  cdj3lem1  33029  f1od2  33304  xrpxdivcld  33494  xrge0npcan  33574  elrgspnlem2  33797  rlocf1  33828  resvid2  33884  resvval2  33885  qsdrng  34014  r1pquslmic  34135  0mplrim  34139  selvply1rhmlemb  34144  selvply1rhmlem2  34146  selvply1rhmlem4  34148  mplvrpmmhm  34171  mplvrpmrhm  34172  esplyfval0  34189  esplyfvaln  34199  vietalem  34204  rtelextdg2lem  34351  esumsnf  34689  esummulc1  34706  measxun2  34836  omsmeas  34948  sibfof  34965  probun  35044  signstfvn  35191  bnj517  35508  ex-sategoelel  36165  mrsubfval  36252  msrval  36282  dfrdg2  36537  itgeq12i  36975  mh-inf3f1  37309  bj-prmoore  38016  bj-bary1lem1  38212  rdgeqoa  38273  finxpreclem2  38293  finxpreclem3  38296  poimirlem1  38519  poimirlem2  38520  poimirlem3  38521  poimirlem4  38522  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem14  38532  poimirlem15  38533  poimirlem17  38535  poimirlem20  38538  poimirlem22  38540  poimirlem23  38541  poimirlem24  38542  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  mblfinlem2  38556  mblfinlem3  38557  ismblfin  38559  mbfposadd  38565  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  ftc1anclem8  38598  areacirc  38611  ismtyval  38714  ismrer1  38752  grposnOLD  38796  rabeq12f  39069  csbeq12  39070  iuneq12f  39075  lsatcv1  40085  glbconN  40414  atltcvr  40472  3dim2  40505  islln2a  40554  2at0mat0  40562  islpln2a  40585  islvol2aN  40629  pmodlem2  40884  pmapjat1  40890  pcl0bN  40960  osumclN  41004  pexmidALTN  41015  lhp2at0nle  41072  4atexlemunv  41103  cdleme18b  41329  cdleme31sn1  41418  cdleme31sde  41422  cdleme31sn2  41426  ltrniotavalbN  41621  trljco  41777  cdlemh  41854  cdlemk40t  41955  cdlemk40f  41956  cdleml9  42021  dihmeetlem3N  42342  dochkrshp  42423  dihprrn  42463  dihjat1  42466  dvh3dim  42483  dochkrsm  42495  dochexmid  42505  lcfl7lem  42536  lcfl9a  42542  lclkrlem1  42543  mapdspex  42705  mapdindp2  42758  mapdh6dN  42776  hdmap1l6d  42850  hdmap11lem2  42879  hdmap14lem4a  42908  hdmapip0  42952  hlhilset  42971  mulgt0b2d  43522  fiabv  43580  0prjspnrel  43643  jm2.26a  43986  onov0suclim  44260  oe0suclim  44263  cantnfresb  44310  onmcl  44317  omcl2  44319  tfsconcatun  44323  naddwordnexlem4  44387  mnringmulrcld  45211  radcnvrat  45283  sumsnd  46012  icccncfext  46866  fperdvper  46898  dvcosax  46905  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  volioc  46951  itgiccshift  46959  stoweidlem34  47013  dirkercncflem2  47083  fourierdlem32  47118  fourierdlem41  47127  fourierdlem48  47133  fourierdlem64  47149  fourierdlem73  47158  fourierdlem79  47164  fourierdlem82  47167  fourierdlem97  47182  fourierdlem101  47186  fourierdlem109  47194  fourierdlem111  47196  fouriersw  47210  elaa2  47213  etransclem24  47237  etransclem25  47238  etransclem46  47259  nnfoctbdjlem  47434  ismeannd  47446  smfpimltxr  47726  smfpimgtxr  47759  ndfatafv2undef  48251  fzopredsuc  48363  m1modmmod  48403  modlt0b  48408  prproropf1olem3  48556  prproropf1olem4  48557  fmtnorec2lem  48596  2pwp1prmfmtno  48644  sfprmdvdsmersenne  48657  sgprmdvdsmersenne  48658  lighneallem2  48660  lighneallem3  48661  ppivalnnprm  48679  ppivalnnnprmge6  48680  dfodd6  48704  dfeven4  48705  m1expevenALTV  48714  isubgredg  48933  upgrimwlklem5  48968  gricushgr  48984  stgrusgra  49026  isubgr3stgrlem8  49040  clintopval  49270  lmod0rng  49295  zlidlring  49300  2zrngagrp  49315  dmmpossx2  49418  zlmodzxzscm  49438  zlmodzxzadd  49439  domnmsuppn0  49450  rmsuppss  49451  scmsuppss  49452  ply1mulgsumlem4  49470  ldepsprlem  49553  lincresunit2  49559  nn0sumshdiglemB  49701  2arymptfv  49731  ackval42  49777  affinecomb1  49783  itschlc0yqe  49841  itsclquadb  49857  2itscp  49862  incat  50678  0setrec  50766