Theorem sylan9eqr 2801

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  sbcied2  3758  csbied2  3868  opthhausdorff0  5426  fun2ssres  6463  fcoi1  6632  fcoi2  6633  funssfv  6777  fvtp1  7052  nvof1o  7133  onuninsuci  7662  ot1stg  7818  ot2ndg  7819  el2xptp0  7851  mpomptsx  7877  dmmpossx  7879  fmpox  7880  2ndconst  7912  offsplitfpar  7931  mpoxopoveq  8006  wfrlem10OLD  8120  rdgeq12  8215  rdgsucmptnf  8231  frsucmptn  8240  oev2  8315  oesuclem  8317  oawordeulem  8347  om00  8368  omass  8373  omeulem1  8375  oeoa  8390  oeoe  8392  nnmass  8417  oaabs2  8439  omabs  8441  mapsnend  8780  omxpenlem  8813  sbthlem4  8826  sbthlem6  8828  fodomr  8864  ssenen  8887  fi0  9109  cantnfp1  9369  cnfcomlem  9387  cardaleph  9776  cflim2  9950  axdc4lem  10142  fpwwe2lem11  10328  fpwwe2lem12  10329  rankcf  10464  inatsk  10465  ltrnq  10666  addclprlem1  10703  mulclprlem  10706  1idpr  10716  prlem936  10734  reclem3pr  10736  mulcmpblnrlem  10757  recexsrlem  10790  map2psrpr  10797  addid0  11324  subdivcomb2  11601  nnnn0addcl  12193  zindd  12351  qaddcl  12634  qmulcl  12636  qreccl  12638  xaddnemnf  12899  xaddnepnf  12900  xaddcom  12903  xnegdi  12911  xaddass  12912  xpncan  12914  xleadd1a  12916  xlt2add  12923  rexmul  12934  xmulgt0  12946  xmulge0  12947  xmulasslem3  12949  xlemul1a  12951  xadddilem  12957  xadddi2  12960  modmuladd  13561  modm1p1mod0  13570  modfzo0difsn  13591  seqf1olem2  13691  expp1  13717  expneg  13718  expcllem  13721  mulexp  13750  expmul  13756  sqoddm1div8  13886  bcpasc  13963  hashrabsn01  14016  fseq1hash  14019  hashinfxadd  14028  hashfzo  14072  fnfz0hash  14086  ffzo0hash  14089  hashf1lem1  14096  hashf1lem1OLD  14097  hashge2el2dif  14122  hashdifsnp1  14138  lsw0  14196  ccatval1  14209  ccatval1OLD  14210  ccatval2  14211  swrdval  14284  ccatopth  14357  reuccatpfxs1  14388  splval  14392  repswswrd  14425  2cshwcshw  14466  s4dom  14560  wrdlen2i  14583  shftfn  14712  reim0b  14758  cjexp  14789  sqeqd  14805  fsumser  15370  sumsnf  15383  binomlem  15469  expcnv  15504  prodsn  15600  prodsnf  15602  bpolylem  15686  bpoly2  15695  bpoly3  15696  ef0lem  15716  dvdsnegb  15911  mod2eq1n2dvds  15984  m1expe  16011  m1expo  16012  m1exp1  16013  flodddiv4  16050  sadadd2lem2  16085  gcdabsOLD  16167  bezoutr1  16202  dvdslcm  16231  lcmeq0  16233  lcmcl  16234  lcmabs  16238  lcmgcdlem  16239  lcmdvds  16241  lcmf0val  16255  lcmftp  16269  lcmfunsnlem2  16273  mulgcddvds  16288  divgcdcoprmex  16299  pcge0  16491  pcadd  16518  pcmpt2  16522  prmreclem4  16548  ramval  16637  ramcl  16658  fvprmselelfz  16673  fvprmselgcd1  16674  ressid2  16871  ressval2  16872  mndind  18381  frmdval  18405  efmnd  18424  smndex1igid  18458  smndex1n0mnd  18466  mgm2nsgrplem3  18474  mulgfval  18617  mulgfvalALT  18618  mulgnn0subcl  18632  mulgnn0z  18645  cycsubm  18736  isga  18812  symgextfve  18942  symgfixf1  18960  f1omvdco2  18971  psgnsn  19043  odid  19061  gexid  19101  efgsval2  19254  frgpuptinv  19292  frgpup2  19297  dprdsn  19554  srgmulgass  19682  srgpcomp  19683  srgbinomlem4  19694  ringinvnzdiv  19747  f1ghm0to0  19899  f1rhm0to0ALT  19900  isabvd  19995  issrng  20025  lmodvsmmulgdi  20073  mptscmfsupp0  20103  lvecinv  20290  lspdisj2  20304  lspfixed  20305  lspexch  20306  sralem  20354  sralemOLD  20355  srasca  20362  sravsca  20363  sraip  20364  znval  20651  psgndiflemB  20717  isphl  20745  assamulgscmlem2  21014  mplval  21107  opsrval  21157  cply1mul  21375  gsummoncoe1  21385  evl1fval  21404  scmate  21567  scmatscm  21570  mdetdiagid  21657  mdetunilem7  21675  mdetuni0  21678  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  slesolinvbi  21738  cpmatacl  21773  cpmatinvcl  21774  pmatcollpw2lem  21834  monmatcollpw  21836  pmatcollpwfi  21839  mp2pm2mplem4  21866  pm2mp  21882  cpmadugsumlemF  21933  cpmadugsumfi  21934  cpmadumatpoly  21940  cayhamlem4  21945  cayleyhamilton0  21946  cayleyhamiltonALT  21948  indistopon  22059  0ntr  22130  pnrmopn  22402  reftr  22573  kgenval  22594  pt1hmeo  22865  fmval  23002  fmf  23004  istmd  23133  istgp  23136  tsmsval2  23189  isxmet2d  23388  xpsxmetlem  23440  xpsmet  23443  blfvalps  23444  tmsval  23542  isnlm  23745  nmoleub  23801  idnghm  23813  blssioo  23864  blcvx  23867  icccvx  24019  pcorevlem  24095  isclm  24133  caufval  24344  iscms  24414  mbfsup  24733  i1f1  24759  dvexp3  25047  rolle  25059  dvivth  25079  deg1add  25173  0dgr  25311  coefv0  25314  elqaalem2  25385  dvradcnv  25485  abelthlem8  25503  efper  25541  logtayl  25720  abscxpbnd  25811  relogbcxpb  25842  logbgcd1irr  25849  dcubic2  25899  rlimcnp2  26021  cvxcl  26039  zetacvg  26069  lgamgulmlem2  26084  vmaval  26167  chtub  26265  logexprlim  26278  dchrsum2  26321  sumdchr2  26323  bposlem2  26338  lgsdir  26385  lgsne0  26388  lgsdirnn0  26397  lgsdinn0  26398  lgsquadlem2  26434  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgslem3a1  26453  2lgslem3b1  26454  2lgslem3c1  26455  2lgslem3d1  26456  2sqn0  26487  dchrvmasum2if  26550  dchrvmasumiflem1  26554  rpvmasum2  26565  pntpbnd1  26639  ostth2lem4  26689  trgcgrg  26780  tgcgr4  26796  ax5seglem1  27199  ax5seglem2  27200  ax5seglem5  27204  usgr1vr  27525  cplgr2vpr  27703  cplgr3v  27705  cusgrrusgr  27851  wlklenvm1  27891  wlk0prc  27923  wlksoneq1eq2  27934  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  crctcshlem4  28086  crctcsh  28090  wlkiswwlks1  28133  wwlksnext  28159  wwlksnextbi  28160  wwlksnextwrd  28163  midwwlks2s3  28218  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2a4  28262  clwlkclwwlklem3  28266  clwwisshclwws  28280  erclwwlkeqlen  28284  clwwlkinwwlk  28305  clwwlkn2  28309  clwwlkf  28312  clwwlkf1  28314  eleclclwwlknlem2  28326  erclwwlkneqlen  28333  umgrhashecclwwlk  28343  eucrctshift  28508  eucrct2eupth  28510  fusgr2wsp2nb  28599  grpoidinvlem2  28768  vcz  28838  nvz  28932  lnon0  29061  ipasslem2  29095  htthlem  29180  hvpncan  29302  hiidge0  29361  normgt0  29390  hsn0elch  29511  shsel3  29578  spansneleq  29833  normcan  29839  h1datomi  29844  fh1  29881  spansncvi  29915  5oalem1  29917  5oalem3  29919  5oalem5  29921  3oalem2  29926  pjdsi  29975  kbpj  30219  0hmop  30246  0lnfn  30248  adj0  30257  nlelshi  30323  branmfn  30368  opsqrlem1  30403  hst1h  30490  mdsl0  30573  superpos  30617  sumdmdlem  30681  cdj3lem1  30697  f1od2  30958  xrpxdivcld  31111  xrge0npcan  31205  resvid2  31429  resvval2  31430  esumsnf  31932  esummulc1  31949  measxun2  32078  omsmeas  32190  sibfof  32207  probun  32286  signstfvn  32448  bnj517  32765  pthhashvtx  32989  ex-sategoelel  33283  mrsubfval  33370  msrval  33400  dfrdg2  33677  ttrclselem2  33712  bj-prmoore  35213  bj-bary1lem1  35409  rdgeqoa  35468  finxpreclem2  35488  finxpreclem3  35491  matunitlindflem1  35700  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem14  35718  poimirlem15  35719  poimirlem17  35721  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  mbfposadd  35751  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  ftc1anclem8  35784  areacirc  35797  ismtyval  35885  ismrer1  35923  grposnOLD  35967  rabeq12f  36242  csbeq12  36243  iuneq12f  36248  lsatcv1  36989  glbconN  37318  atltcvr  37376  3dim2  37409  islln2a  37458  2at0mat0  37466  islpln2a  37489  islvol2aN  37533  pmodlem2  37788  pmapjat1  37794  pcl0bN  37864  osumclN  37908  pexmidALTN  37919  lhp2at0nle  37976  4atexlemunv  38007  cdleme18b  38233  cdleme31sn1  38322  cdleme31sde  38326  cdleme31sn2  38330  ltrniotavalbN  38525  trljco  38681  cdlemh  38758  cdlemk40t  38859  cdlemk40f  38860  cdleml9  38925  dihmeetlem3N  39246  dochkrshp  39327  dihprrn  39367  dihjat1  39370  dvh3dim  39387  dochkrsm  39399  dochexmid  39409  lcfl7lem  39440  lcfl9a  39446  lclkrlem1  39447  mapdspex  39609  mapdindp2  39662  mapdh6dN  39680  hdmap1l6d  39754  hdmap11lem2  39783  hdmap14lem4a  39812  hdmapip0  39856  hlhilset  39875  nnadd1com  40218  sn-negex12  40319  prjspner1  40384  0prjspnrel  40385  jm2.26a  40738  mnringmulrcld  41735  radcnvrat  41821  sumsnd  42458  icccncfext  43318  fperdvper  43350  dvcosax  43357  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  volioc  43403  itgiccshift  43411  stoweidlem34  43465  dirkercncflem2  43535  fourierdlem32  43570  fourierdlem41  43579  fourierdlem48  43585  fourierdlem64  43601  fourierdlem73  43610  fourierdlem79  43616  fourierdlem82  43619  fourierdlem97  43634  fourierdlem101  43638  fourierdlem109  43646  fourierdlem111  43648  fouriersw  43662  elaa2  43665  etransclem24  43689  etransclem25  43690  etransclem46  43711  nnfoctbdjlem  43883  ismeannd  43895  ndfatafv2undef  44591  fzopredsuc  44703  prproropf1olem3  44845  prproropf1olem4  44846  fmtnorec2lem  44882  2pwp1prmfmtno  44930  sfprmdvdsmersenne  44943  sgprmdvdsmersenne  44944  lighneallem2  44946  lighneallem3  44947  dfodd6  44977  dfeven4  44978  m1expevenALTV  44987  isomushgr  45166  isomuspgrlem2d  45171  clintopval  45286  lmod0rng  45314  zlidlring  45374  2zrngagrp  45389  rngcval  45408  ringcval  45454  dmmpossx2  45560  zlmodzxzscm  45581  zlmodzxzadd  45582  domnmsuppn0  45593  rmsuppss  45594  scmsuppss  45596  ply1mulgsumlem4  45618  ldepsprlem  45701  lincresunit2  45707  m1modmmod  45755  nn0sumshdiglemB  45854  2arymptfv  45884  ackval42  45930  affinecomb1  45936  itschlc0yqe  45994  itsclquadb  46010  2itscp  46015  0setrec  46295