Theorem sylan9eqr 2794

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  sbcied2  3774  csbied2  3875  opthhausdorff0  5466  fun2ssres  6537  fcoi1  6708  fcoi2  6709  funssfv  6855  fvtp1  7143  nvof1o  7228  onuninsuci  7784  ot1stg  7949  ot2ndg  7950  el2xptp0  7982  mpomptsx  8010  dmmpossx  8012  fmpox  8013  2ndconst  8044  offsplitfpar  8062  mpoxopoveq  8162  rdgeq12  8345  rdgsucmptnf  8361  frsucmptn  8371  oev2  8451  oesuclem  8453  oawordeulem  8482  om00  8503  omass  8508  omeulem1  8510  oeoa  8526  oeoe  8528  nnmass  8553  oaabs2  8578  omabs  8580  mapsnend  8976  omxpenlem  9009  sbthlem4  9021  sbthlem6  9023  fodomr  9059  ssenen  9082  fodomfir  9231  fi0  9326  cantnfp1  9593  cnfcomlem  9611  ttrclselem2  9638  cardaleph  10002  cflim2  10176  axdc4lem  10368  fpwwe2lem11  10555  fpwwe2lem12  10556  rankcf  10691  inatsk  10692  ltrnq  10893  addclprlem1  10930  mulclprlem  10933  1idpr  10943  prlem936  10961  reclem3pr  10963  mulcmpblnrlem  10984  recexsrlem  11017  map2psrpr  11024  addid0  11560  subdivcomb2  11842  nnadd1com  12191  nnnn0addcl  12458  zindd  12621  qaddcl  12906  qmulcl  12908  qreccl  12910  xaddnemnf  13179  xaddnepnf  13180  xaddcom  13183  xnegdi  13191  xaddass  13192  xpncan  13194  xleadd1a  13196  xlt2add  13203  rexmul  13214  xmulgt0  13226  xmulge0  13227  xmulasslem3  13229  xlemul1a  13231  xadddilem  13237  xadddi2  13240  modmuladd  13866  modm1p1mod0  13875  modfzo0difsn  13896  seqf1olem2  13995  expp1  14021  expneg  14022  expcllem  14025  mulexp  14054  expmul  14060  sqoddm1div8  14196  bcpasc  14274  hashrabsn01  14326  fseq1hash  14329  hashinfxadd  14338  hashfzo  14382  fnfz0hash  14399  ffzo0hash  14402  hashf1lem1  14408  hashge2el2dif  14433  hash3tpexb  14447  hashdifsnp1  14459  lsw0  14518  ccatval1  14530  ccatval2  14531  swrdval  14597  ccatopth  14669  reuccatpfxs1  14700  splval  14704  repswswrd  14737  2cshwcshw  14778  s4dom  14872  wrdlen2i  14895  shftfn  15026  reim0b  15072  cjexp  15103  sqeqd  15119  fsumser  15683  sumsnf  15696  binomlem  15785  expcnv  15820  prodsn  15918  prodsnf  15920  bpolylem  16004  bpoly2  16013  bpoly3  16014  ef0lem  16034  dvdsnegb  16233  mod2eq1n2dvds  16307  m1expe  16334  m1expo  16335  m1exp1  16336  flodddiv4  16375  sadadd2lem2  16410  bezoutr1  16529  dvdslcm  16558  lcmeq0  16560  lcmcl  16561  lcmabs  16565  lcmgcdlem  16566  lcmdvds  16568  lcmf0val  16582  lcmftp  16596  lcmfunsnlem2  16600  mulgcddvds  16615  divgcdcoprmex  16626  pcge0  16824  pcadd  16851  pcmpt2  16855  prmreclem4  16881  ramval  16970  ramcl  16991  fvprmselelfz  17006  fvprmselgcd1  17007  ressid2  17195  ressval2  17196  mndind  18787  frmdval  18810  efmnd  18829  smndex1igid  18865  smndex1igidOLD  18866  smndex1n0mnd  18874  mgm2nsgrplem3  18882  mulgfval  19036  mulgfvalALT  19037  mulgnn0subcl  19054  mulgnn0z  19068  cycsubm  19168  f1ghm0to0  19211  isga  19257  symgextfve  19385  symgfixf1  19403  f1omvdco2  19414  psgnsn  19486  odid  19504  gexid  19547  efgsval2  19699  frgpuptinv  19737  frgpup2  19742  dprdsn  20004  srgmulgass  20189  srgpcomp  20190  srgbinomlem4  20201  ringinvnzdiv  20273  rngcval  20586  ringcval  20615  isabvd  20780  issrng  20812  lmodvsmmulgdi  20883  mptscmfsupp0  20913  lvecinv  21103  lspdisj2  21117  lspfixed  21118  lspexch  21119  sralem  21163  srasca  21167  sravsca  21168  sraip  21169  znval  21525  psgndiflemB  21590  isphl  21618  assamulgscmlem2  21890  mplval  21977  opsrval  22034  psdmvr  22145  cply1mul  22271  gsummoncoe1  22283  evl1fval  22303  scmate  22485  scmatscm  22488  mdetdiagid  22575  mdetunilem7  22593  mdetuni0  22596  gsummatr01lem3  22632  gsummatr01lem4  22633  gsummatr01  22634  slesolinvbi  22656  cpmatacl  22691  cpmatinvcl  22692  pmatcollpw2lem  22752  monmatcollpw  22754  pmatcollpwfi  22757  mp2pm2mplem4  22784  pm2mp  22800  cpmadugsumlemF  22851  cpmadugsumfi  22852  cpmadumatpoly  22858  cayhamlem4  22863  cayleyhamilton0  22864  cayleyhamiltonALT  22866  indistopon  22976  0ntr  23046  pnrmopn  23318  reftr  23489  kgenval  23510  pt1hmeo  23781  fmval  23918  fmf  23920  istmd  24049  istgp  24052  tsmsval2  24105  isxmet2d  24302  xpsxmetlem  24354  xpsmet  24357  blfvalps  24358  tmsval  24456  isnlm  24650  nmoleub  24706  idnghm  24718  blssioo  24770  blcvx  24773  icccvx  24927  pcorevlem  25003  isclm  25041  caufval  25252  iscms  25322  mbfsup  25641  i1f1  25667  dvexp3  25955  rolle  25967  dvivth  25987  deg1add  26078  0dgr  26220  coefv0  26223  elqaalem2  26297  dvradcnv  26399  abelthlem8  26417  efper  26456  logtayl  26637  abscxpbnd  26730  relogbcxpb  26764  logbgcd1irr  26771  dcubic2  26821  rlimcnp2  26943  cvxcl  26962  zetacvg  26992  lgamgulmlem2  27007  vmaval  27090  chtub  27189  logexprlim  27202  dchrsum2  27245  sumdchr2  27247  bposlem2  27262  lgsdir  27309  lgsne0  27312  lgsdirnn0  27321  lgsdinn0  27322  lgsquadlem2  27358  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2lgslem3a1  27377  2lgslem3b1  27378  2lgslem3c1  27379  2lgslem3d1  27380  2sqn0  27411  dchrvmasum2if  27474  dchrvmasumiflem1  27478  rpvmasum2  27489  pntpbnd1  27563  ostth2lem4  27613  expsp1  28435  trgcgrg  28597  tgcgr4  28613  ax5seglem1  29011  ax5seglem2  29012  ax5seglem5  29016  usgr1vr  29338  cplgr2vpr  29516  cplgr3v  29518  cusgrrusgr  29665  wlklenvm1  29705  wlk0prc  29736  wlksoneq1eq2  29746  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  crctcshwlkn0lem6  29898  crctcshlem4  29903  crctcsh  29907  wlkiswwlks1  29950  wwlksnext  29976  wwlksnextbi  29977  wwlksnextwrd  29980  midwwlks2s3  30035  clwlkclwwlklem2fv1  30080  clwlkclwwlklem2a4  30082  clwlkclwwlklem3  30086  clwwisshclwws  30100  erclwwlkeqlen  30104  clwwlkinwwlk  30125  clwwlkn2  30129  clwwlkf  30132  clwwlkf1  30134  eleclclwwlknlem2  30146  erclwwlkneqlen  30153  umgrhashecclwwlk  30163  eucrctshift  30328  eucrct2eupth  30330  fusgr2wsp2nb  30419  grpoidinvlem2  30591  vcz  30661  nvz  30755  lnon0  30884  ipasslem2  30918  htthlem  31003  hvpncan  31125  hiidge0  31184  normgt0  31213  hsn0elch  31334  shsel3  31401  spansneleq  31656  normcan  31662  h1datomi  31667  fh1  31704  spansncvi  31738  5oalem1  31740  5oalem3  31742  5oalem5  31744  3oalem2  31749  pjdsi  31798  kbpj  32042  0hmop  32069  0lnfn  32071  adj0  32080  nlelshi  32146  branmfn  32191  opsqrlem1  32226  hst1h  32313  mdsl0  32396  superpos  32440  sumdmdlem  32504  cdj3lem1  32520  f1od2  32807  xrpxdivcld  33009  xrge0npcan  33095  elrgspnlem2  33319  rlocf1  33349  resvid2  33405  resvval2  33406  qsdrng  33572  r1pquslmic  33686  mplvrpmmhm  33705  mplvrpmrhm  33706  esplyfval0  33723  esplyfvaln  33733  vietalem  33738  rtelextdg2lem  33886  esumsnf  34224  esummulc1  34241  measxun2  34370  omsmeas  34483  sibfof  34500  probun  34579  signstfvn  34729  bnj517  35043  pthhashvtx  35326  ex-sategoelel  35619  mrsubfval  35706  msrval  35736  dfrdg2  35991  itgeq12i  36404  bj-prmoore  37443  bj-bary1lem1  37641  rdgeqoa  37700  finxpreclem2  37720  finxpreclem3  37723  matunitlindflem1  37951  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem14  37969  poimirlem15  37970  poimirlem17  37972  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  mblfinlem2  37993  mblfinlem3  37994  ismblfin  37996  mbfposadd  38002  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  ftc1anclem8  38035  areacirc  38048  ismtyval  38135  ismrer1  38173  grposnOLD  38217  rabeq12f  38492  csbeq12  38493  iuneq12f  38498  lsatcv1  39508  glbconN  39837  atltcvr  39895  3dim2  39928  islln2a  39977  2at0mat0  39985  islpln2a  40008  islvol2aN  40052  pmodlem2  40307  pmapjat1  40313  pcl0bN  40383  osumclN  40427  pexmidALTN  40438  lhp2at0nle  40495  4atexlemunv  40526  cdleme18b  40752  cdleme31sn1  40841  cdleme31sde  40845  cdleme31sn2  40849  ltrniotavalbN  41044  trljco  41200  cdlemh  41277  cdlemk40t  41378  cdlemk40f  41379  cdleml9  41444  dihmeetlem3N  41765  dochkrshp  41846  dihprrn  41886  dihjat1  41889  dvh3dim  41906  dochkrsm  41918  dochexmid  41928  lcfl7lem  41959  lcfl9a  41965  lclkrlem1  41966  mapdspex  42128  mapdindp2  42181  mapdh6dN  42199  hdmap1l6d  42273  hdmap11lem2  42302  hdmap14lem4a  42331  hdmapip0  42375  hlhilset  42394  mulgt0b2d  42937  fiabv  42995  prjspner1  43073  0prjspnrel  43074  jm2.26a  43446  onov0suclim  43720  oe0suclim  43723  cantnfresb  43770  onmcl  43777  omcl2  43779  tfsconcatun  43783  naddwordnexlem4  43847  mnringmulrcld  44673  radcnvrat  44759  sumsnd  45475  icccncfext  46333  fperdvper  46365  dvcosax  46372  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  volioc  46418  itgiccshift  46426  stoweidlem34  46480  dirkercncflem2  46550  fourierdlem32  46585  fourierdlem41  46594  fourierdlem48  46600  fourierdlem64  46616  fourierdlem73  46625  fourierdlem79  46631  fourierdlem82  46634  fourierdlem97  46649  fourierdlem101  46653  fourierdlem109  46661  fourierdlem111  46663  fouriersw  46677  elaa2  46680  etransclem24  46704  etransclem25  46705  etransclem46  46726  nnfoctbdjlem  46901  ismeannd  46913  smfpimltxr  47193  smfpimgtxr  47226  ndfatafv2undef  47672  fzopredsuc  47784  m1modmmod  47824  modlt0b  47829  prproropf1olem3  47977  prproropf1olem4  47978  fmtnorec2lem  48017  2pwp1prmfmtno  48065  sfprmdvdsmersenne  48078  sgprmdvdsmersenne  48079  lighneallem2  48081  lighneallem3  48082  ppivalnnprm  48100  ppivalnnnprmge6  48101  dfodd6  48125  dfeven4  48126  m1expevenALTV  48135  isubgredg  48354  upgrimwlklem5  48389  gricushgr  48405  stgrusgra  48447  isubgr3stgrlem8  48461  clintopval  48692  lmod0rng  48717  zlidlring  48722  2zrngagrp  48737  dmmpossx2  48825  zlmodzxzscm  48845  zlmodzxzadd  48846  domnmsuppn0  48857  rmsuppss  48858  scmsuppss  48859  ply1mulgsumlem4  48877  ldepsprlem  48960  lincresunit2  48966  nn0sumshdiglemB  49108  2arymptfv  49138  ackval42  49184  affinecomb1  49190  itschlc0yqe  49248  itsclquadb  49264  2itscp  49269  incat  50088  0setrec  50191