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  5459  fun2ssres  6530  fcoi1  6701  fcoi2  6702  funssfv  6848  fvtp1  7139  nvof1o  7224  onuninsuci  7780  ot1stg  7945  ot2ndg  7946  el2xptp0  7978  mpomptsx  8006  dmmpossx  8008  fmpox  8009  2ndconst  8040  offsplitfpar  8058  mpoxopoveq  8159  rdgeq12  8342  rdgsucmptnf  8358  frsucmptn  8368  oev2  8448  oesuclem  8450  oawordeulem  8479  om00  8500  omass  8505  omeulem1  8507  oeoa  8523  oeoe  8525  nnmass  8550  oaabs2  8575  omabs  8577  mapsnend  8973  omxpenlem  9006  sbthlem4  9018  sbthlem6  9020  fodomr  9056  ssenen  9079  fodomfir  9228  fi0  9323  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  20590  ringcval  20619  isabvd  20784  issrng  20816  lmodvsmmulgdi  20887  mptscmfsupp0  20917  lvecinv  21106  lspdisj2  21120  lspfixed  21121  lspexch  21122  sralem  21166  srasca  21170  sravsca  21171  sraip  21172  znval  21510  psgndiflemB  21575  isphl  21603  assamulgscmlem2  21875  mplval  21963  opsrval  22022  psdmvr  22157  cply1mul  22282  gsummoncoe1  22294  evl1fval  22314  scmate  22493  scmatscm  22496  mdetdiagid  22583  mdetunilem7  22601  mdetuni0  22604  gsummatr01lem3  22640  gsummatr01lem4  22641  gsummatr01  22642  slesolinvbi  22664  cpmatacl  22699  cpmatinvcl  22700  pmatcollpw2lem  22760  monmatcollpw  22762  pmatcollpwfi  22765  mp2pm2mplem4  22792  pm2mp  22808  cpmadugsumlemF  22859  cpmadugsumfi  22860  cpmadumatpoly  22866  cayhamlem4  22871  cayleyhamilton0  22872  cayleyhamiltonALT  22874  indistopon  22984  0ntr  23054  pnrmopn  23326  reftr  23497  kgenval  23518  pt1hmeo  23789  fmval  23926  fmf  23928  istmd  24057  istgp  24060  tsmsval2  24113  isxmet2d  24310  xpsxmetlem  24362  xpsmet  24365  blfvalps  24366  tmsval  24464  isnlm  24658  nmoleub  24714  idnghm  24726  blssioo  24778  blcvx  24781  icccvx  24935  pcorevlem  25011  isclm  25049  caufval  25260  iscms  25330  mbfsup  25649  i1f1  25675  dvexp3  25963  rolle  25975  dvivth  25995  deg1add  26086  0dgr  26228  coefv0  26231  elqaalem2  26304  dvradcnv  26404  abelthlem8  26422  efper  26461  logtayl  26642  abscxpbnd  26735  relogbcxpb  26769  logbgcd1irr  26776  dcubic2  26826  rlimcnp2  26948  cvxcl  26966  zetacvg  26996  lgamgulmlem2  27011  vmaval  27094  chtub  27193  logexprlim  27206  dchrsum2  27249  sumdchr2  27251  bposlem2  27266  lgsdir  27313  lgsne0  27316  lgsdirnn0  27325  lgsdinn0  27326  lgsquadlem2  27362  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2lgslem3a1  27381  2lgslem3b1  27382  2lgslem3c1  27383  2lgslem3d1  27384  2sqn0  27415  dchrvmasum2if  27478  dchrvmasumiflem1  27482  rpvmasum2  27493  pntpbnd1  27567  ostth2lem4  27617  expsp1  28439  trgcgrg  28601  tgcgr4  28617  ax5seglem1  29015  ax5seglem2  29016  ax5seglem5  29020  usgr1vr  29342  cplgr2vpr  29520  cplgr3v  29522  cusgrrusgr  29668  wlklenvm1  29708  wlk0prc  29739  wlksoneq1eq2  29749  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  crctcshlem4  29906  crctcsh  29910  wlkiswwlks1  29953  wwlksnext  29979  wwlksnextbi  29980  wwlksnextwrd  29983  midwwlks2s3  30038  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2a4  30085  clwlkclwwlklem3  30089  clwwisshclwws  30103  erclwwlkeqlen  30107  clwwlkinwwlk  30128  clwwlkn2  30132  clwwlkf  30135  clwwlkf1  30137  eleclclwwlknlem2  30149  erclwwlkneqlen  30156  umgrhashecclwwlk  30166  eucrctshift  30331  eucrct2eupth  30333  fusgr2wsp2nb  30422  grpoidinvlem2  30594  vcz  30664  nvz  30758  lnon0  30887  ipasslem2  30921  htthlem  31006  hvpncan  31128  hiidge0  31187  normgt0  31216  hsn0elch  31337  shsel3  31404  spansneleq  31659  normcan  31665  h1datomi  31670  fh1  31707  spansncvi  31741  5oalem1  31743  5oalem3  31745  5oalem5  31747  3oalem2  31752  pjdsi  31801  kbpj  32045  0hmop  32072  0lnfn  32074  adj0  32083  nlelshi  32149  branmfn  32194  opsqrlem1  32229  hst1h  32316  mdsl0  32399  superpos  32443  sumdmdlem  32507  cdj3lem1  32523  f1od2  32811  xrpxdivcld  33013  xrge0npcan  33099  elrgspnlem2  33324  rlocf1  33354  resvid2  33413  resvval2  33414  qsdrng  33580  r1pquslmic  33694  0mplrim  33698  selvply1rhmlemb  33703  selvply1rhmlem2  33705  selvply1rhmlem4  33707  mplvrpmmhm  33730  mplvrpmrhm  33731  esplyfval0  33748  esplyfvaln  33758  vietalem  33763  rtelextdg2lem  33910  esumsnf  34248  esummulc1  34265  measxun2  34394  omsmeas  34507  sibfof  34524  probun  34603  signstfvn  34753  bnj517  35067  pthhashvtx  35356  ex-sategoelel  35649  mrsubfval  35736  msrval  35766  dfrdg2  36021  itgeq12i  36434  bj-prmoore  37473  bj-bary1lem1  37671  rdgeqoa  37732  finxpreclem2  37752  finxpreclem3  37755  matunitlindflem1  37983  poimirlem1  37988  poimirlem2  37989  poimirlem3  37990  poimirlem4  37991  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem14  38001  poimirlem15  38002  poimirlem17  38004  poimirlem20  38007  poimirlem22  38009  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  mblfinlem2  38025  mblfinlem3  38026  ismblfin  38028  mbfposadd  38034  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  ftc1anclem8  38067  areacirc  38080  ismtyval  38167  ismrer1  38205  grposnOLD  38249  rabeq12f  38524  csbeq12  38525  iuneq12f  38530  lsatcv1  39540  glbconN  39869  atltcvr  39927  3dim2  39960  islln2a  40009  2at0mat0  40017  islpln2a  40040  islvol2aN  40084  pmodlem2  40339  pmapjat1  40345  pcl0bN  40415  osumclN  40459  pexmidALTN  40470  lhp2at0nle  40527  4atexlemunv  40558  cdleme18b  40784  cdleme31sn1  40873  cdleme31sde  40877  cdleme31sn2  40881  ltrniotavalbN  41076  trljco  41232  cdlemh  41309  cdlemk40t  41410  cdlemk40f  41411  cdleml9  41476  dihmeetlem3N  41797  dochkrshp  41878  dihprrn  41918  dihjat1  41921  dvh3dim  41938  dochkrsm  41950  dochexmid  41960  lcfl7lem  41991  lcfl9a  41997  lclkrlem1  41998  mapdspex  42160  mapdindp2  42213  mapdh6dN  42231  hdmap1l6d  42305  hdmap11lem2  42334  hdmap14lem4a  42363  hdmapip0  42407  hlhilset  42426  mulgt0b2d  42968  fiabv  43022  prjspner1  43076  0prjspnrel  43077  jm2.26a  43445  onov0suclim  43719  oe0suclim  43722  cantnfresb  43769  onmcl  43776  omcl2  43778  tfsconcatun  43782  naddwordnexlem4  43846  mnringmulrcld  44672  radcnvrat  44758  sumsnd  45474  icccncfext  46330  fperdvper  46362  dvcosax  46369  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  volioc  46415  itgiccshift  46423  stoweidlem34  46477  dirkercncflem2  46547  fourierdlem32  46582  fourierdlem41  46591  fourierdlem48  46597  fourierdlem64  46613  fourierdlem73  46622  fourierdlem79  46628  fourierdlem82  46631  fourierdlem97  46646  fourierdlem101  46650  fourierdlem109  46658  fourierdlem111  46660  fouriersw  46674  elaa2  46677  etransclem24  46701  etransclem25  46702  etransclem46  46723  nnfoctbdjlem  46898  ismeannd  46910  smfpimltxr  47190  smfpimgtxr  47223  ndfatafv2undef  47675  fzopredsuc  47787  m1modmmod  47827  modlt0b  47832  prproropf1olem3  47980  prproropf1olem4  47981  fmtnorec2lem  48020  2pwp1prmfmtno  48068  sfprmdvdsmersenne  48081  sgprmdvdsmersenne  48082  lighneallem2  48084  lighneallem3  48085  ppivalnnprm  48103  ppivalnnnprmge6  48104  dfodd6  48128  dfeven4  48129  m1expevenALTV  48138  isubgredg  48357  upgrimwlklem5  48392  gricushgr  48408  stgrusgra  48450  isubgr3stgrlem8  48464  clintopval  48695  lmod0rng  48720  zlidlring  48725  2zrngagrp  48740  dmmpossx2  48828  zlmodzxzscm  48848  zlmodzxzadd  48849  domnmsuppn0  48860  rmsuppss  48861  scmsuppss  48862  ply1mulgsumlem4  48880  ldepsprlem  48963  lincresunit2  48969  nn0sumshdiglemB  49111  2arymptfv  49141  ackval42  49187  affinecomb1  49193  itschlc0yqe  49251  itsclquadb  49267  2itscp  49272  incat  50091  0setrec  50194