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 459	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  sbcied2  3764  csbied2  3873  opthhausdorff0  5433  fun2ssres  6486  fcoi1  6657  fcoi2  6658  funssfv  6804  fvtp1  7079  nvof1o  7161  onuninsuci  7696  ot1stg  7854  ot2ndg  7855  el2xptp0  7887  mpomptsx  7913  dmmpossx  7915  fmpox  7916  2ndconst  7950  offsplitfpar  7969  mpoxopoveq  8044  wfrlem10OLD  8158  rdgeq12  8253  rdgsucmptnf  8269  frsucmptn  8279  oev2  8362  oesuclem  8364  oawordeulem  8394  om00  8415  omass  8420  omeulem1  8422  oeoa  8437  oeoe  8439  nnmass  8464  oaabs2  8488  omabs  8490  mapsnend  8835  omxpenlem  8869  sbthlem4  8882  sbthlem6  8884  fodomr  8924  ssenen  8947  fi0  9188  cantnfp1  9448  cnfcomlem  9466  ttrclselem2  9493  cardaleph  9854  cflim2  10028  axdc4lem  10220  fpwwe2lem11  10406  fpwwe2lem12  10407  rankcf  10542  inatsk  10543  ltrnq  10744  addclprlem1  10781  mulclprlem  10784  1idpr  10794  prlem936  10812  reclem3pr  10814  mulcmpblnrlem  10835  recexsrlem  10868  map2psrpr  10875  addid0  11403  subdivcomb2  11680  nnnn0addcl  12272  zindd  12430  qaddcl  12714  qmulcl  12716  qreccl  12718  xaddnemnf  12979  xaddnepnf  12980  xaddcom  12983  xnegdi  12991  xaddass  12992  xpncan  12994  xleadd1a  12996  xlt2add  13003  rexmul  13014  xmulgt0  13026  xmulge0  13027  xmulasslem3  13029  xlemul1a  13031  xadddilem  13037  xadddi2  13040  modmuladd  13642  modm1p1mod0  13651  modfzo0difsn  13672  seqf1olem2  13772  expp1  13798  expneg  13799  expcllem  13802  mulexp  13831  expmul  13837  sqoddm1div8  13967  bcpasc  14044  hashrabsn01  14097  fseq1hash  14100  hashinfxadd  14109  hashfzo  14153  fnfz0hash  14167  ffzo0hash  14170  hashf1lem1  14177  hashf1lem1OLD  14178  hashge2el2dif  14203  hashdifsnp1  14219  lsw0  14277  ccatval1  14290  ccatval1OLD  14291  ccatval2  14292  swrdval  14365  ccatopth  14438  reuccatpfxs1  14469  splval  14473  repswswrd  14506  2cshwcshw  14547  s4dom  14641  wrdlen2i  14664  shftfn  14793  reim0b  14839  cjexp  14870  sqeqd  14886  fsumser  15451  sumsnf  15464  binomlem  15550  expcnv  15585  prodsn  15681  prodsnf  15683  bpolylem  15767  bpoly2  15776  bpoly3  15777  ef0lem  15797  dvdsnegb  15992  mod2eq1n2dvds  16065  m1expe  16092  m1expo  16093  m1exp1  16094  flodddiv4  16131  sadadd2lem2  16166  gcdabsOLD  16248  bezoutr1  16283  dvdslcm  16312  lcmeq0  16314  lcmcl  16315  lcmabs  16319  lcmgcdlem  16320  lcmdvds  16322  lcmf0val  16336  lcmftp  16350  lcmfunsnlem2  16354  mulgcddvds  16369  divgcdcoprmex  16380  pcge0  16572  pcadd  16599  pcmpt2  16603  prmreclem4  16629  ramval  16718  ramcl  16739  fvprmselelfz  16754  fvprmselgcd1  16755  ressid2  16954  ressval2  16955  mndind  18475  frmdval  18499  efmnd  18518  smndex1igid  18552  smndex1n0mnd  18560  mgm2nsgrplem3  18568  mulgfval  18711  mulgfvalALT  18712  mulgnn0subcl  18726  mulgnn0z  18739  cycsubm  18830  isga  18906  symgextfve  19036  symgfixf1  19054  f1omvdco2  19065  psgnsn  19137  odid  19155  gexid  19195  efgsval2  19348  frgpuptinv  19386  frgpup2  19391  dprdsn  19648  srgmulgass  19776  srgpcomp  19777  srgbinomlem4  19788  ringinvnzdiv  19841  f1ghm0to0  19993  f1rhm0to0ALT  19994  isabvd  20089  issrng  20119  lmodvsmmulgdi  20167  mptscmfsupp0  20197  lvecinv  20384  lspdisj2  20398  lspfixed  20399  lspexch  20400  sralem  20448  sralemOLD  20449  srasca  20456  srascaOLD  20457  sravsca  20458  sravscaOLD  20459  sraip  20460  znval  20748  psgndiflemB  20814  isphl  20842  assamulgscmlem2  21113  mplval  21206  opsrval  21256  cply1mul  21474  gsummoncoe1  21484  evl1fval  21503  scmate  21668  scmatscm  21671  mdetdiagid  21758  mdetunilem7  21776  mdetuni0  21779  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  slesolinvbi  21839  cpmatacl  21874  cpmatinvcl  21875  pmatcollpw2lem  21935  monmatcollpw  21937  pmatcollpwfi  21940  mp2pm2mplem4  21967  pm2mp  21983  cpmadugsumlemF  22034  cpmadugsumfi  22035  cpmadumatpoly  22041  cayhamlem4  22046  cayleyhamilton0  22047  cayleyhamiltonALT  22049  indistopon  22160  0ntr  22231  pnrmopn  22503  reftr  22674  kgenval  22695  pt1hmeo  22966  fmval  23103  fmf  23105  istmd  23234  istgp  23237  tsmsval2  23290  isxmet2d  23489  xpsxmetlem  23541  xpsmet  23544  blfvalps  23545  tmsval  23645  isnlm  23848  nmoleub  23904  idnghm  23916  blssioo  23967  blcvx  23970  icccvx  24122  pcorevlem  24198  isclm  24236  caufval  24448  iscms  24518  mbfsup  24837  i1f1  24863  dvexp3  25151  rolle  25163  dvivth  25183  deg1add  25277  0dgr  25415  coefv0  25418  elqaalem2  25489  dvradcnv  25589  abelthlem8  25607  efper  25645  logtayl  25824  abscxpbnd  25915  relogbcxpb  25946  logbgcd1irr  25953  dcubic2  26003  rlimcnp2  26125  cvxcl  26143  zetacvg  26173  lgamgulmlem2  26188  vmaval  26271  chtub  26369  logexprlim  26382  dchrsum2  26425  sumdchr2  26427  bposlem2  26442  lgsdir  26489  lgsne0  26492  lgsdirnn0  26501  lgsdinn0  26502  lgsquadlem2  26538  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2lgslem3a1  26557  2lgslem3b1  26558  2lgslem3c1  26559  2lgslem3d1  26560  2sqn0  26591  dchrvmasum2if  26654  dchrvmasumiflem1  26658  rpvmasum2  26669  pntpbnd1  26743  ostth2lem4  26793  trgcgrg  26885  tgcgr4  26901  ax5seglem1  27305  ax5seglem2  27306  ax5seglem5  27310  usgr1vr  27631  cplgr2vpr  27809  cplgr3v  27811  cusgrrusgr  27957  wlklenvm1  27998  wlk0prc  28030  wlksoneq1eq2  28041  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem6  28189  crctcshlem4  28194  crctcsh  28198  wlkiswwlks1  28241  wwlksnext  28267  wwlksnextbi  28268  wwlksnextwrd  28271  midwwlks2s3  28326  clwlkclwwlklem2fv1  28368  clwlkclwwlklem2a4  28370  clwlkclwwlklem3  28374  clwwisshclwws  28388  erclwwlkeqlen  28392  clwwlkinwwlk  28413  clwwlkn2  28417  clwwlkf  28420  clwwlkf1  28422  eleclclwwlknlem2  28434  erclwwlkneqlen  28441  umgrhashecclwwlk  28451  eucrctshift  28616  eucrct2eupth  28618  fusgr2wsp2nb  28707  grpoidinvlem2  28876  vcz  28946  nvz  29040  lnon0  29169  ipasslem2  29203  htthlem  29288  hvpncan  29410  hiidge0  29469  normgt0  29498  hsn0elch  29619  shsel3  29686  spansneleq  29941  normcan  29947  h1datomi  29952  fh1  29989  spansncvi  30023  5oalem1  30025  5oalem3  30027  5oalem5  30029  3oalem2  30034  pjdsi  30083  kbpj  30327  0hmop  30354  0lnfn  30356  adj0  30365  nlelshi  30431  branmfn  30476  opsqrlem1  30511  hst1h  30598  mdsl0  30681  superpos  30725  sumdmdlem  30789  cdj3lem1  30805  f1od2  31065  xrpxdivcld  31218  xrge0npcan  31312  resvid2  31536  resvval2  31537  esumsnf  32041  esummulc1  32058  measxun2  32187  omsmeas  32299  sibfof  32316  probun  32395  signstfvn  32557  bnj517  32874  pthhashvtx  33098  ex-sategoelel  33392  mrsubfval  33479  msrval  33509  dfrdg2  33780  bj-prmoore  35295  bj-bary1lem1  35491  rdgeqoa  35550  finxpreclem2  35570  finxpreclem3  35573  matunitlindflem1  35782  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem14  35800  poimirlem15  35801  poimirlem17  35803  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  mbfposadd  35833  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  ftc1anclem8  35866  areacirc  35879  ismtyval  35967  ismrer1  36005  grposnOLD  36049  rabeq12f  36324  csbeq12  36325  iuneq12f  36330  lsatcv1  37069  glbconN  37398  atltcvr  37456  3dim2  37489  islln2a  37538  2at0mat0  37546  islpln2a  37569  islvol2aN  37613  pmodlem2  37868  pmapjat1  37874  pcl0bN  37944  osumclN  37988  pexmidALTN  37999  lhp2at0nle  38056  4atexlemunv  38087  cdleme18b  38313  cdleme31sn1  38402  cdleme31sde  38406  cdleme31sn2  38410  ltrniotavalbN  38605  trljco  38761  cdlemh  38838  cdlemk40t  38939  cdlemk40f  38940  cdleml9  39005  dihmeetlem3N  39326  dochkrshp  39407  dihprrn  39447  dihjat1  39450  dvh3dim  39467  dochkrsm  39479  dochexmid  39489  lcfl7lem  39520  lcfl9a  39526  lclkrlem1  39527  mapdspex  39689  mapdindp2  39742  mapdh6dN  39760  hdmap1l6d  39834  hdmap11lem2  39863  hdmap14lem4a  39892  hdmapip0  39936  hlhilset  39955  nnadd1com  40304  sn-negex12  40405  prjspner1  40470  0prjspnrel  40471  jm2.26a  40829  mnringmulrcld  41853  radcnvrat  41939  sumsnd  42576  icccncfext  43435  fperdvper  43467  dvcosax  43474  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  volioc  43520  itgiccshift  43528  stoweidlem34  43582  dirkercncflem2  43652  fourierdlem32  43687  fourierdlem41  43696  fourierdlem48  43702  fourierdlem64  43718  fourierdlem73  43727  fourierdlem79  43733  fourierdlem82  43736  fourierdlem97  43751  fourierdlem101  43755  fourierdlem109  43763  fourierdlem111  43765  fouriersw  43779  elaa2  43782  etransclem24  43806  etransclem25  43807  etransclem46  43828  nnfoctbdjlem  44000  ismeannd  44012  smfpimltxr  44292  smfpimgtxr  44325  ndfatafv2undef  44715  fzopredsuc  44826  prproropf1olem3  44968  prproropf1olem4  44969  fmtnorec2lem  45005  2pwp1prmfmtno  45053  sfprmdvdsmersenne  45066  sgprmdvdsmersenne  45067  lighneallem2  45069  lighneallem3  45070  dfodd6  45100  dfeven4  45101  m1expevenALTV  45110  isomushgr  45289  isomuspgrlem2d  45294  clintopval  45409  lmod0rng  45437  zlidlring  45497  2zrngagrp  45512  rngcval  45531  ringcval  45577  dmmpossx2  45683  zlmodzxzscm  45704  zlmodzxzadd  45705  domnmsuppn0  45716  rmsuppss  45717  scmsuppss  45719  ply1mulgsumlem4  45741  ldepsprlem  45824  lincresunit2  45830  m1modmmod  45878  nn0sumshdiglemB  45977  2arymptfv  46007  ackval42  46053  affinecomb1  46059  itschlc0yqe  46117  itsclquadb  46133  2itscp  46138  0setrec  46420