Theorem sylan9eqr 2817

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 2815	. 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 2732

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

This theorem is used by:  sbcied2  3783  csbied2  3884  opthhausdorff0  5495  fun2ssres  6578  fcoi1  6749  fcoi2  6750  funssfv  6899  fvtp1  7193  nvof1o  7281  onuninsuci  7836  ot1stg  8000  ot2ndg  8001  el2xptp0  8033  mpomptsx  8061  dmmpossx  8063  fmpox  8064  2ndconst  8098  offsplitfpar  8116  mpoxopoveq  8217  rdgeq12  8402  rdgsucmptnf  8418  frsucmptn  8428  oev2  8510  oesuclem  8512  oawordeulem  8541  om00  8562  omass  8567  omeulem1  8569  oeoa  8585  oeoe  8587  nnmass  8612  oaabs2  8637  omabs  8639  mapsnend  9043  omxpenlem  9076  sbthlem4  9088  sbthlem6  9090  fodomr  9126  ssenen  9149  fodomfir  9297  fi0  9390  cantnfp1  9660  cnfcomlem  9678  ttrclselem2  9705  cardaleph  10092  cflim2  10265  axdc4lem  10457  fpwwe2lem11  10650  fpwwe2lem12  10651  rankcf  10786  inatsk  10787  ltrnq  10988  addclprlem1  11025  mulclprlem  11028  1idpr  11038  prlem936  11056  reclem3pr  11058  mulcmpblnrlem  11079  recexsrlem  11112  map2psrpr  11119  addid0  11657  subdivcomb2  11935  nnadd1com  12283  nnnn0addcl  12558  zindd  12722  qaddcl  13015  qmulcl  13017  qreccl  13019  xaddnemnf  13288  xaddnepnf  13289  xaddcom  13292  xnegdi  13300  xaddass  13301  xpncan  13303  xleadd1a  13305  xlt2add  13312  rexmul  13323  xmulgt0  13335  xmulge0  13336  xmulasslem3  13338  xlemul1a  13340  xadddilem  13346  xadddi2  13349  modmuladd  13977  modm1p1mod0  13986  modfzo0difsn  14007  seqf1olem2  14106  expp1  14132  expneg  14133  expcllem  14136  mulexp  14165  expmul  14171  sqoddm1div8  14307  bcpasc  14385  hashrabsn01  14437  fseq1hash  14440  hashinfxadd  14449  hashfzo  14494  fnfz0hash  14511  ffzo0hash  14514  hashf1lem1  14520  hashge2el2dif  14545  hash3tpexb  14559  hashdifsnp1  14571  lsw0  14630  ccatval1  14642  ccatval2  14643  swrdval  14711  ccatopth  14785  reuccatpfxs1  14816  splval  14820  repswswrd  14855  2cshwcshw  14896  s4dom  14990  wrdlen2i  15013  shftfn  15146  reim0b  15206  cjexp  15237  sqeqd  15253  fsumser  15816  sumsnf  15829  binomlem  15918  expcnv  15953  prodsn  16049  prodsnf  16051  bpolylem  16134  bpoly2  16143  bpoly3  16144  ef0lem  16164  dvdsnegb  16363  mod2eq1n2dvds  16437  m1expe  16464  m1expo  16465  m1exp1  16466  flodddiv4  16505  sadadd2lem2  16540  bezoutr1  16659  dvdslcm  16688  lcmeq0  16690  lcmcl  16691  lcmabs  16695  lcmgcdlem  16696  lcmdvds  16698  lcmf0val  16712  lcmftp  16726  lcmfunsnlem2  16730  mulgcddvds  16745  divgcdcoprmex  16756  pcge0  16954  pcadd  16981  pcmpt2  16985  prmreclem4  17011  ramval  17100  ramcl  17121  fvprmselelfz  17136  fvprmselgcd1  17137  ressid2  17326  ressval2  17327  mndind  18937  frmdval  18960  efmnd  18979  smndex1igid  19015  smndex1igidOLD  19016  smndex1n0mnd  19024  mgm2nsgrplem3  19032  mulgfval  19192  mulgfvalALT  19193  mulgnn0subcl  19210  mulgnn0z  19224  cycsubm  19330  f1ghm0to0  19372  isga  19418  symgextfve  19546  symgfixf1  19564  f1omvdco2  19575  psgnsn  19647  odid  19665  gexid  19708  efgsval2  19860  frgpuptinv  19898  frgpup2  19903  dprdsn  20165  srgmulgass  20356  srgpcomp  20357  srgbinomlem4  20368  ringinvnzdiv  20443  rngcval  20780  ringcval  20809  isabvd  20978  issrng  21010  lmodvsmmulgdi  21081  mptscmfsupp0  21111  lvecinv  21300  lspdisj2  21314  lspfixed  21315  lspexch  21316  sralem  21360  srasca  21364  sravsca  21365  sraip  21366  znval  21748  psgndiflemB  21813  isphl  21841  assamulgscmlem2  22115  mplval  22203  opsrval  22262  psdmvr  22397  cply1mul  22521  gsummoncoe1  22533  evl1fval  22553  scmate  22732  scmatscm  22735  mdetdiagid  22822  mdetunilem7  22840  mdetuni0  22843  gsummatr01lem3  22879  gsummatr01lem4  22880  gsummatr01  22881  matunitlindflem1  22901  slesolinvbi  22906  cpmatacl  22941  cpmatinvcl  22942  pmatcollpw2lem  23002  monmatcollpw  23004  pmatcollpwfi  23007  mp2pm2mplem4  23034  pm2mp  23050  cpmadugsumlemF  23101  cpmadugsumfi  23102  cpmadumatpoly  23108  cayhamlem4  23113  cayleyhamilton0  23114  cayleyhamiltonALT  23116  indistopon  23226  0ntr  23296  pnrmopn  23568  reftr  23740  kgenval  23761  pt1hmeo  24032  fmval  24169  fmf  24171  istmd  24300  istgp  24303  tsmsval2  24356  isxmet2d  24553  xpsxmetlem  24605  xpsmet  24608  blfvalps  24609  tmsval  24707  isnlm  24901  nmoleub  24957  idnghm  24969  blssioo  25021  blcvx  25024  icccvx  25178  pcorevlem  25254  isclm  25292  caufval  25503  iscms  25573  mbfsup  25892  i1f1  25918  dvexp3  26205  rolle  26217  dvivth  26237  deg1add  26328  0dgr  26471  coefv0  26474  elqaalem2  26552  dvradcnv  26657  abelthlem8  26675  efper  26717  logtayl  26897  abscxpbnd  26990  relogbcxpb  27024  logbgcd1irr  27031  dcubic2  27081  rlimcnp2  27203  cvxcl  27221  zetacvg  27251  lgamgulmlem2  27266  vmaval  27349  chtub  27448  logexprlim  27461  dchrsum2  27504  sumdchr2  27506  bposlem2  27521  lgsdir  27568  lgsne0  27571  lgsdirnn0  27580  lgsdinn0  27581  lgsquadlem2  27617  2lgslem3a  27632  2lgslem3b  27633  2lgslem3c  27634  2lgslem3d  27635  2lgslem3a1  27636  2lgslem3b1  27637  2lgslem3c1  27638  2lgslem3d1  27639  2sqn0  27670  dchrvmasum2if  27733  dchrvmasumiflem1  27737  rpvmasum2  27748  pntpbnd1  27822  ostth2lem4  27872  expsp1  28694  trgcgrg  28857  tgcgr4  28873  ax5seglem1  29385  ax5seglem2  29386  ax5seglem5  29390  usgr1vr  29715  cplgr2vpr  29893  cplgr3v  29895  cusgrrusgr  30041  wlklenvm1  30081  wlk0prc  30112  wlksoneq1eq2  30122  pthhashvtx  30194  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  crctcshwlkn0lem6  30283  crctcshlem4  30288  crctcsh  30292  wlkiswwlks1  30335  wwlksnext  30361  wwlksnextbi  30362  wwlksnextwrd  30365  midwwlks2s3  30420  clwlkclwwlklem2fv1  30465  clwlkclwwlklem2a4  30467  clwlkclwwlklem3  30471  clwwisshclwws  30485  erclwwlkeqlen  30489  clwwlkinwwlk  30510  clwwlkn2  30514  clwwlkf  30517  clwwlkf1  30519  eleclclwwlknlem2  30531  erclwwlkneqlen  30538  umgrhashecclwwlk  30548  eucrctshift  30723  eucrct2eupth  30725  fusgr2wsp2nb  30814  grpoidinvlem2  30986  vcz  31056  nvz  31150  lnon0  31279  ipasslem2  31313  htthlem  31398  hvpncan  31520  hiidge0  31579  normgt0  31608  hsn0elch  31729  shsel3  31796  spansneleq  32051  normcan  32057  h1datomi  32062  fh1  32099  spansncvi  32133  5oalem1  32135  5oalem3  32137  5oalem5  32139  3oalem2  32144  pjdsi  32193  kbpj  32437  0hmop  32464  0lnfn  32466  adj0  32475  nlelshi  32541  branmfn  32586  opsqrlem1  32621  hst1h  32708  mdsl0  32791  superpos  32835  sumdmdlem  32899  cdj3lem1  32915  f1od2  33190  xrpxdivcld  33380  xrge0npcan  33460  elrgspnlem2  33683  rlocf1  33714  resvid2  33770  resvval2  33771  qsdrng  33899  r1pquslmic  34020  0mplrim  34024  selvply1rhmlemb  34029  selvply1rhmlem2  34031  selvply1rhmlem4  34033  mplvrpmmhm  34056  mplvrpmrhm  34057  esplyfval0  34074  esplyfvaln  34084  vietalem  34089  rtelextdg2lem  34236  esumsnf  34574  esummulc1  34591  measxun2  34721  omsmeas  34834  sibfof  34851  probun  34930  signstfvn  35077  bnj517  35394  ex-sategoelel  36000  mrsubfval  36087  msrval  36117  dfrdg2  36372  itgeq12i  36826  bj-prmoore  37865  bj-bary1lem1  38063  rdgeqoa  38124  finxpreclem2  38144  finxpreclem3  38147  poimirlem1  38370  poimirlem2  38371  poimirlem3  38372  poimirlem4  38373  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem14  38383  poimirlem15  38384  poimirlem17  38386  poimirlem20  38389  poimirlem22  38391  poimirlem23  38392  poimirlem24  38393  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  mblfinlem2  38407  mblfinlem3  38408  ismblfin  38410  mbfposadd  38416  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  ftc1anclem8  38449  areacirc  38462  ismtyval  38550  ismrer1  38588  grposnOLD  38632  rabeq12f  38905  csbeq12  38906  iuneq12f  38911  lsatcv1  39921  glbconN  40250  atltcvr  40308  3dim2  40341  islln2a  40390  2at0mat0  40398  islpln2a  40421  islvol2aN  40465  pmodlem2  40720  pmapjat1  40726  pcl0bN  40796  osumclN  40840  pexmidALTN  40851  lhp2at0nle  40908  4atexlemunv  40939  cdleme18b  41165  cdleme31sn1  41254  cdleme31sde  41258  cdleme31sn2  41262  ltrniotavalbN  41457  trljco  41613  cdlemh  41690  cdlemk40t  41791  cdlemk40f  41792  cdleml9  41857  dihmeetlem3N  42178  dochkrshp  42259  dihprrn  42299  dihjat1  42302  dvh3dim  42319  dochkrsm  42331  dochexmid  42341  lcfl7lem  42372  lcfl9a  42378  lclkrlem1  42379  mapdspex  42541  mapdindp2  42594  mapdh6dN  42612  hdmap1l6d  42686  hdmap11lem2  42715  hdmap14lem4a  42744  hdmapip0  42788  hlhilset  42807  mulgt0b2d  43366  fiabv  43418  prjspner1  43472  0prjspnrel  43473  jm2.26a  43841  onov0suclim  44115  oe0suclim  44118  cantnfresb  44165  onmcl  44172  omcl2  44174  tfsconcatun  44178  naddwordnexlem4  44242  mnringmulrcld  45066  radcnvrat  45138  sumsnd  45860  icccncfext  46715  fperdvper  46747  dvcosax  46754  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  volioc  46800  itgiccshift  46808  stoweidlem34  46862  dirkercncflem2  46932  fourierdlem32  46967  fourierdlem41  46976  fourierdlem48  46982  fourierdlem64  46998  fourierdlem73  47007  fourierdlem79  47013  fourierdlem82  47016  fourierdlem97  47031  fourierdlem101  47035  fourierdlem109  47043  fourierdlem111  47045  fouriersw  47059  elaa2  47062  etransclem24  47086  etransclem25  47087  etransclem46  47108  nnfoctbdjlem  47283  ismeannd  47295  smfpimltxr  47575  smfpimgtxr  47608  ndfatafv2undef  48100  fzopredsuc  48212  m1modmmod  48252  modlt0b  48257  prproropf1olem3  48405  prproropf1olem4  48406  fmtnorec2lem  48445  2pwp1prmfmtno  48493  sfprmdvdsmersenne  48506  sgprmdvdsmersenne  48507  lighneallem2  48509  lighneallem3  48510  ppivalnnprm  48528  ppivalnnnprmge6  48529  dfodd6  48553  dfeven4  48554  m1expevenALTV  48563  isubgredg  48782  upgrimwlklem5  48817  gricushgr  48833  stgrusgra  48875  isubgr3stgrlem8  48889  clintopval  49119  lmod0rng  49144  zlidlring  49149  2zrngagrp  49164  dmmpossx2  49267  zlmodzxzscm  49287  zlmodzxzadd  49288  domnmsuppn0  49299  rmsuppss  49300  scmsuppss  49301  ply1mulgsumlem4  49319  ldepsprlem  49402  lincresunit2  49408  nn0sumshdiglemB  49550  2arymptfv  49580  ackval42  49626  affinecomb1  49632  itschlc0yqe  49690  itsclquadb  49706  2itscp  49711  incat  50527  0setrec  50630