Theorem sylan9eqr 2796

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  sbcied2  3767  csbied2  3868  opthhausdorff0  5460  fun2ssres  6531  fcoi1  6702  fcoi2  6703  funssfv  6849  fvtp1  7140  nvof1o  7225  onuninsuci  7781  ot1stg  7946  ot2ndg  7947  el2xptp0  7979  mpomptsx  8007  dmmpossx  8009  fmpox  8010  2ndconst  8041  offsplitfpar  8059  mpoxopoveq  8160  rdgeq12  8343  rdgsucmptnf  8359  frsucmptn  8369  oev2  8449  oesuclem  8451  oawordeulem  8480  om00  8501  omass  8506  omeulem1  8508  oeoa  8524  oeoe  8526  nnmass  8551  oaabs2  8576  omabs  8578  mapsnend  8974  omxpenlem  9007  sbthlem4  9019  sbthlem6  9021  fodomr  9057  ssenen  9080  fodomfir  9229  fi0  9324  cantnfp1  9594  cnfcomlem  9612  ttrclselem2  9639  cardaleph  10003  cflim2  10177  axdc4lem  10369  fpwwe2lem11  10556  fpwwe2lem12  10557  rankcf  10692  inatsk  10693  ltrnq  10894  addclprlem1  10931  mulclprlem  10934  1idpr  10944  prlem936  10962  reclem3pr  10964  mulcmpblnrlem  10985  recexsrlem  11018  map2psrpr  11025  addid0  11561  subdivcomb2  11843  nnadd1com  12192  nnnn0addcl  12459  zindd  12622  qaddcl  12907  qmulcl  12909  qreccl  12911  xaddnemnf  13180  xaddnepnf  13181  xaddcom  13184  xnegdi  13192  xaddass  13193  xpncan  13195  xleadd1a  13197  xlt2add  13204  rexmul  13215  xmulgt0  13227  xmulge0  13228  xmulasslem3  13230  xlemul1a  13232  xadddilem  13238  xadddi2  13241  modmuladd  13867  modm1p1mod0  13876  modfzo0difsn  13897  seqf1olem2  13996  expp1  14022  expneg  14023  expcllem  14026  mulexp  14055  expmul  14061  sqoddm1div8  14197  bcpasc  14275  hashrabsn01  14327  fseq1hash  14330  hashinfxadd  14339  hashfzo  14383  fnfz0hash  14400  ffzo0hash  14403  hashf1lem1  14409  hashge2el2dif  14434  hash3tpexb  14448  hashdifsnp1  14460  lsw0  14519  ccatval1  14531  ccatval2  14532  swrdval  14598  ccatopth  14670  reuccatpfxs1  14701  splval  14705  repswswrd  14738  2cshwcshw  14779  s4dom  14873  wrdlen2i  14896  shftfn  15027  reim0b  15073  cjexp  15104  sqeqd  15120  fsumser  15684  sumsnf  15697  binomlem  15786  expcnv  15821  prodsn  15919  prodsnf  15921  bpolylem  16005  bpoly2  16014  bpoly3  16015  ef0lem  16035  dvdsnegb  16234  mod2eq1n2dvds  16308  m1expe  16335  m1expo  16336  m1exp1  16337  flodddiv4  16376  sadadd2lem2  16411  bezoutr1  16530  dvdslcm  16559  lcmeq0  16561  lcmcl  16562  lcmabs  16566  lcmgcdlem  16567  lcmdvds  16569  lcmf0val  16583  lcmftp  16597  lcmfunsnlem2  16601  mulgcddvds  16616  divgcdcoprmex  16627  pcge0  16825  pcadd  16852  pcmpt2  16856  prmreclem4  16882  ramval  16971  ramcl  16992  fvprmselelfz  17007  fvprmselgcd1  17008  ressid2  17196  ressval2  17197  mndind  18788  frmdval  18811  efmnd  18830  smndex1igid  18866  smndex1igidOLD  18867  smndex1n0mnd  18875  mgm2nsgrplem3  18883  mulgfval  19037  mulgfvalALT  19038  mulgnn0subcl  19055  mulgnn0z  19069  cycsubm  19169  f1ghm0to0  19212  isga  19258  symgextfve  19386  symgfixf1  19404  f1omvdco2  19415  psgnsn  19487  odid  19505  gexid  19548  efgsval2  19700  frgpuptinv  19738  frgpup2  19743  dprdsn  20005  srgmulgass  20190  srgpcomp  20191  srgbinomlem4  20202  ringinvnzdiv  20274  rngcval  20591  ringcval  20620  isabvd  20785  issrng  20817  lmodvsmmulgdi  20888  mptscmfsupp0  20918  lvecinv  21107  lspdisj2  21121  lspfixed  21122  lspexch  21123  sralem  21167  srasca  21171  sravsca  21172  sraip  21173  znval  21511  psgndiflemB  21576  isphl  21604  assamulgscmlem2  21876  mplval  21964  opsrval  22023  psdmvr  22158  cply1mul  22283  gsummoncoe1  22295  evl1fval  22315  scmate  22494  scmatscm  22497  mdetdiagid  22584  mdetunilem7  22602  mdetuni0  22605  gsummatr01lem3  22641  gsummatr01lem4  22642  gsummatr01  22643  slesolinvbi  22665  cpmatacl  22700  cpmatinvcl  22701  pmatcollpw2lem  22761  monmatcollpw  22763  pmatcollpwfi  22766  mp2pm2mplem4  22793  pm2mp  22809  cpmadugsumlemF  22860  cpmadugsumfi  22861  cpmadumatpoly  22867  cayhamlem4  22872  cayleyhamilton0  22873  cayleyhamiltonALT  22875  indistopon  22985  0ntr  23055  pnrmopn  23327  reftr  23498  kgenval  23519  pt1hmeo  23790  fmval  23927  fmf  23929  istmd  24058  istgp  24061  tsmsval2  24114  isxmet2d  24311  xpsxmetlem  24363  xpsmet  24366  blfvalps  24367  tmsval  24465  isnlm  24659  nmoleub  24715  idnghm  24727  blssioo  24779  blcvx  24782  icccvx  24936  pcorevlem  25012  isclm  25050  caufval  25261  iscms  25331  mbfsup  25650  i1f1  25676  dvexp3  25964  rolle  25976  dvivth  25996  deg1add  26087  0dgr  26229  coefv0  26232  elqaalem2  26305  dvradcnv  26405  abelthlem8  26423  efper  26462  logtayl  26643  abscxpbnd  26736  relogbcxpb  26770  logbgcd1irr  26777  dcubic2  26827  rlimcnp2  26949  cvxcl  26967  zetacvg  26997  lgamgulmlem2  27012  vmaval  27095  chtub  27194  logexprlim  27207  dchrsum2  27250  sumdchr2  27252  bposlem2  27267  lgsdir  27314  lgsne0  27317  lgsdirnn0  27326  lgsdinn0  27327  lgsquadlem2  27363  2lgslem3a  27378  2lgslem3b  27379  2lgslem3c  27380  2lgslem3d  27381  2lgslem3a1  27382  2lgslem3b1  27383  2lgslem3c1  27384  2lgslem3d1  27385  2sqn0  27416  dchrvmasum2if  27479  dchrvmasumiflem1  27483  rpvmasum2  27494  pntpbnd1  27568  ostth2lem4  27618  expsp1  28440  trgcgrg  28602  tgcgr4  28618  ax5seglem1  29016  ax5seglem2  29017  ax5seglem5  29021  usgr1vr  29343  cplgr2vpr  29521  cplgr3v  29523  cusgrrusgr  29669  wlklenvm1  29709  wlk0prc  29740  wlksoneq1eq2  29750  crctcshwlkn0lem4  29900  crctcshwlkn0lem5  29901  crctcshwlkn0lem6  29902  crctcshlem4  29907  crctcsh  29911  wlkiswwlks1  29954  wwlksnext  29980  wwlksnextbi  29981  wwlksnextwrd  29984  midwwlks2s3  30039  clwlkclwwlklem2fv1  30084  clwlkclwwlklem2a4  30086  clwlkclwwlklem3  30090  clwwisshclwws  30104  erclwwlkeqlen  30108  clwwlkinwwlk  30129  clwwlkn2  30133  clwwlkf  30136  clwwlkf1  30138  eleclclwwlknlem2  30150  erclwwlkneqlen  30157  umgrhashecclwwlk  30167  eucrctshift  30332  eucrct2eupth  30334  fusgr2wsp2nb  30423  grpoidinvlem2  30595  vcz  30665  nvz  30759  lnon0  30888  ipasslem2  30922  htthlem  31007  hvpncan  31129  hiidge0  31188  normgt0  31217  hsn0elch  31338  shsel3  31405  spansneleq  31660  normcan  31666  h1datomi  31671  fh1  31708  spansncvi  31742  5oalem1  31744  5oalem3  31746  5oalem5  31748  3oalem2  31753  pjdsi  31802  kbpj  32046  0hmop  32073  0lnfn  32075  adj0  32084  nlelshi  32150  branmfn  32195  opsqrlem1  32230  hst1h  32317  mdsl0  32400  superpos  32444  sumdmdlem  32508  cdj3lem1  32524  f1od2  32812  xrpxdivcld  33014  xrge0npcan  33100  elrgspnlem2  33325  rlocf1  33355  resvid2  33414  resvval2  33415  qsdrng  33581  r1pquslmic  33703  0mplrim  33707  selvply1rhmlemb  33712  selvply1rhmlem2  33714  selvply1rhmlem4  33716  mplvrpmmhm  33739  mplvrpmrhm  33740  esplyfval0  33757  esplyfvaln  33767  vietalem  33772  rtelextdg2lem  33919  esumsnf  34257  esummulc1  34274  measxun2  34403  omsmeas  34516  sibfof  34533  probun  34612  signstfvn  34762  bnj517  35076  pthhashvtx  35365  ex-sategoelel  35658  mrsubfval  35745  msrval  35775  dfrdg2  36030  itgeq12i  36443  bj-prmoore  37482  bj-bary1lem1  37680  rdgeqoa  37741  finxpreclem2  37761  finxpreclem3  37764  matunitlindflem1  37992  poimirlem1  37997  poimirlem2  37998  poimirlem3  37999  poimirlem4  38000  poimirlem5  38001  poimirlem6  38002  poimirlem7  38003  poimirlem10  38006  poimirlem11  38007  poimirlem12  38008  poimirlem14  38010  poimirlem15  38011  poimirlem17  38013  poimirlem20  38016  poimirlem22  38018  poimirlem23  38019  poimirlem24  38020  poimirlem25  38021  poimirlem26  38022  poimirlem27  38023  mblfinlem2  38034  mblfinlem3  38035  ismblfin  38037  mbfposadd  38043  itg2addnclem  38047  itg2addnclem3  38049  itg2addnc  38050  ftc1anclem8  38076  areacirc  38089  ismtyval  38176  ismrer1  38214  grposnOLD  38258  rabeq12f  38533  csbeq12  38534  iuneq12f  38539  lsatcv1  39549  glbconN  39878  atltcvr  39936  3dim2  39969  islln2a  40018  2at0mat0  40026  islpln2a  40049  islvol2aN  40093  pmodlem2  40348  pmapjat1  40354  pcl0bN  40424  osumclN  40468  pexmidALTN  40479  lhp2at0nle  40536  4atexlemunv  40567  cdleme18b  40793  cdleme31sn1  40882  cdleme31sde  40886  cdleme31sn2  40890  ltrniotavalbN  41085  trljco  41241  cdlemh  41318  cdlemk40t  41419  cdlemk40f  41420  cdleml9  41485  dihmeetlem3N  41806  dochkrshp  41887  dihprrn  41927  dihjat1  41930  dvh3dim  41947  dochkrsm  41959  dochexmid  41969  lcfl7lem  42000  lcfl9a  42006  lclkrlem1  42007  mapdspex  42169  mapdindp2  42222  mapdh6dN  42240  hdmap1l6d  42314  hdmap11lem2  42343  hdmap14lem4a  42372  hdmapip0  42416  hlhilset  42435  mulgt0b2d  42977  fiabv  43031  prjspner1  43085  0prjspnrel  43086  jm2.26a  43454  onov0suclim  43728  oe0suclim  43731  cantnfresb  43778  onmcl  43785  omcl2  43787  tfsconcatun  43791  naddwordnexlem4  43855  mnringmulrcld  44681  radcnvrat  44767  sumsnd  45483  icccncfext  46338  fperdvper  46370  dvcosax  46377  ioodvbdlimc1lem1  46382  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  volioc  46423  itgiccshift  46431  stoweidlem34  46485  dirkercncflem2  46555  fourierdlem32  46590  fourierdlem41  46599  fourierdlem48  46605  fourierdlem64  46621  fourierdlem73  46630  fourierdlem79  46636  fourierdlem82  46639  fourierdlem97  46654  fourierdlem101  46658  fourierdlem109  46666  fourierdlem111  46668  fouriersw  46682  elaa2  46685  etransclem24  46709  etransclem25  46710  etransclem46  46731  nnfoctbdjlem  46906  ismeannd  46918  smfpimltxr  47198  smfpimgtxr  47231  ndfatafv2undef  47683  fzopredsuc  47795  m1modmmod  47835  modlt0b  47840  prproropf1olem3  47988  prproropf1olem4  47989  fmtnorec2lem  48028  2pwp1prmfmtno  48076  sfprmdvdsmersenne  48089  sgprmdvdsmersenne  48090  lighneallem2  48092  lighneallem3  48093  ppivalnnprm  48111  ppivalnnnprmge6  48112  dfodd6  48136  dfeven4  48137  m1expevenALTV  48146  isubgredg  48365  upgrimwlklem5  48400  gricushgr  48416  stgrusgra  48458  isubgr3stgrlem8  48472  clintopval  48703  lmod0rng  48728  zlidlring  48733  2zrngagrp  48748  dmmpossx2  48836  zlmodzxzscm  48856  zlmodzxzadd  48857  domnmsuppn0  48868  rmsuppss  48869  scmsuppss  48870  ply1mulgsumlem4  48888  ldepsprlem  48971  lincresunit2  48977  nn0sumshdiglemB  49119  2arymptfv  49149  ackval42  49195  affinecomb1  49201  itschlc0yqe  49259  itsclquadb  49275  2itscp  49280  incat  50099  0setrec  50202