Theorem sylan9eqr 2802

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

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

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 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  sbcied2  3767  csbied2  3877  opthhausdorff0  5436  fun2ssres  6477  fcoi1  6646  fcoi2  6647  funssfv  6792  fvtp1  7067  nvof1o  7149  onuninsuci  7682  ot1stg  7839  ot2ndg  7840  el2xptp0  7872  mpomptsx  7898  dmmpossx  7900  fmpox  7901  2ndconst  7933  offsplitfpar  7952  mpoxopoveq  8027  wfrlem10OLD  8141  rdgeq12  8236  rdgsucmptnf  8252  frsucmptn  8262  oev2  8345  oesuclem  8347  oawordeulem  8377  om00  8398  omass  8403  omeulem1  8405  oeoa  8420  oeoe  8422  nnmass  8447  oaabs2  8471  omabs  8473  mapsnend  8818  omxpenlem  8851  sbthlem4  8864  sbthlem6  8866  fodomr  8906  ssenen  8929  fi0  9167  cantnfp1  9427  cnfcomlem  9445  ttrclselem2  9472  cardaleph  9856  cflim2  10030  axdc4lem  10222  fpwwe2lem11  10408  fpwwe2lem12  10409  rankcf  10544  inatsk  10545  ltrnq  10746  addclprlem1  10783  mulclprlem  10786  1idpr  10796  prlem936  10814  reclem3pr  10816  mulcmpblnrlem  10837  recexsrlem  10870  map2psrpr  10877  addid0  11405  subdivcomb2  11682  nnnn0addcl  12274  zindd  12432  qaddcl  12716  qmulcl  12718  qreccl  12720  xaddnemnf  12981  xaddnepnf  12982  xaddcom  12985  xnegdi  12993  xaddass  12994  xpncan  12996  xleadd1a  12998  xlt2add  13005  rexmul  13016  xmulgt0  13028  xmulge0  13029  xmulasslem3  13031  xlemul1a  13033  xadddilem  13039  xadddi2  13042  modmuladd  13644  modm1p1mod0  13653  modfzo0difsn  13674  seqf1olem2  13774  expp1  13800  expneg  13801  expcllem  13804  mulexp  13833  expmul  13839  sqoddm1div8  13969  bcpasc  14046  hashrabsn01  14099  fseq1hash  14102  hashinfxadd  14111  hashfzo  14155  fnfz0hash  14169  ffzo0hash  14172  hashf1lem1  14179  hashf1lem1OLD  14180  hashge2el2dif  14205  hashdifsnp1  14221  lsw0  14279  ccatval1  14292  ccatval1OLD  14293  ccatval2  14294  swrdval  14367  ccatopth  14440  reuccatpfxs1  14471  splval  14475  repswswrd  14508  2cshwcshw  14549  s4dom  14643  wrdlen2i  14666  shftfn  14795  reim0b  14841  cjexp  14872  sqeqd  14888  fsumser  15453  sumsnf  15466  binomlem  15552  expcnv  15587  prodsn  15683  prodsnf  15685  bpolylem  15769  bpoly2  15778  bpoly3  15779  ef0lem  15799  dvdsnegb  15994  mod2eq1n2dvds  16067  m1expe  16094  m1expo  16095  m1exp1  16096  flodddiv4  16133  sadadd2lem2  16168  gcdabsOLD  16250  bezoutr1  16285  dvdslcm  16314  lcmeq0  16316  lcmcl  16317  lcmabs  16321  lcmgcdlem  16322  lcmdvds  16324  lcmf0val  16338  lcmftp  16352  lcmfunsnlem2  16356  mulgcddvds  16371  divgcdcoprmex  16382  pcge0  16574  pcadd  16601  pcmpt2  16605  prmreclem4  16631  ramval  16720  ramcl  16741  fvprmselelfz  16756  fvprmselgcd1  16757  ressid2  16956  ressval2  16957  mndind  18477  frmdval  18501  efmnd  18520  smndex1igid  18554  smndex1n0mnd  18562  mgm2nsgrplem3  18570  mulgfval  18713  mulgfvalALT  18714  mulgnn0subcl  18728  mulgnn0z  18741  cycsubm  18832  isga  18908  symgextfve  19038  symgfixf1  19056  f1omvdco2  19067  psgnsn  19139  odid  19157  gexid  19197  efgsval2  19350  frgpuptinv  19388  frgpup2  19393  dprdsn  19650  srgmulgass  19778  srgpcomp  19779  srgbinomlem4  19790  ringinvnzdiv  19843  f1ghm0to0  19995  f1rhm0to0ALT  19996  isabvd  20091  issrng  20121  lmodvsmmulgdi  20169  mptscmfsupp0  20199  lvecinv  20386  lspdisj2  20400  lspfixed  20401  lspexch  20402  sralem  20450  sralemOLD  20451  srasca  20458  srascaOLD  20459  sravsca  20460  sravscaOLD  20461  sraip  20462  znval  20750  psgndiflemB  20816  isphl  20844  assamulgscmlem2  21115  mplval  21208  opsrval  21258  cply1mul  21476  gsummoncoe1  21486  evl1fval  21505  scmate  21670  scmatscm  21673  mdetdiagid  21760  mdetunilem7  21778  mdetuni0  21781  gsummatr01lem3  21817  gsummatr01lem4  21818  gsummatr01  21819  slesolinvbi  21841  cpmatacl  21876  cpmatinvcl  21877  pmatcollpw2lem  21937  monmatcollpw  21939  pmatcollpwfi  21942  mp2pm2mplem4  21969  pm2mp  21985  cpmadugsumlemF  22036  cpmadugsumfi  22037  cpmadumatpoly  22043  cayhamlem4  22048  cayleyhamilton0  22049  cayleyhamiltonALT  22051  indistopon  22162  0ntr  22233  pnrmopn  22505  reftr  22676  kgenval  22697  pt1hmeo  22968  fmval  23105  fmf  23107  istmd  23236  istgp  23239  tsmsval2  23292  isxmet2d  23491  xpsxmetlem  23543  xpsmet  23546  blfvalps  23547  tmsval  23647  isnlm  23850  nmoleub  23906  idnghm  23918  blssioo  23969  blcvx  23972  icccvx  24124  pcorevlem  24200  isclm  24238  caufval  24450  iscms  24520  mbfsup  24839  i1f1  24865  dvexp3  25153  rolle  25165  dvivth  25185  deg1add  25279  0dgr  25417  coefv0  25420  elqaalem2  25491  dvradcnv  25591  abelthlem8  25609  efper  25647  logtayl  25826  abscxpbnd  25917  relogbcxpb  25948  logbgcd1irr  25955  dcubic2  26005  rlimcnp2  26127  cvxcl  26145  zetacvg  26175  lgamgulmlem2  26190  vmaval  26273  chtub  26371  logexprlim  26384  dchrsum2  26427  sumdchr2  26429  bposlem2  26444  lgsdir  26491  lgsne0  26494  lgsdirnn0  26503  lgsdinn0  26504  lgsquadlem2  26540  2lgslem3a  26555  2lgslem3b  26556  2lgslem3c  26557  2lgslem3d  26558  2lgslem3a1  26559  2lgslem3b1  26560  2lgslem3c1  26561  2lgslem3d1  26562  2sqn0  26593  dchrvmasum2if  26656  dchrvmasumiflem1  26660  rpvmasum2  26671  pntpbnd1  26745  ostth2lem4  26795  trgcgrg  26887  tgcgr4  26903  ax5seglem1  27307  ax5seglem2  27308  ax5seglem5  27312  usgr1vr  27633  cplgr2vpr  27811  cplgr3v  27813  cusgrrusgr  27959  wlklenvm1  27999  wlk0prc  28031  wlksoneq1eq2  28042  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  37071  glbconN  37400  atltcvr  37458  3dim2  37491  islln2a  37540  2at0mat0  37548  islpln2a  37571  islvol2aN  37615  pmodlem2  37870  pmapjat1  37876  pcl0bN  37946  osumclN  37990  pexmidALTN  38001  lhp2at0nle  38058  4atexlemunv  38089  cdleme18b  38315  cdleme31sn1  38404  cdleme31sde  38408  cdleme31sn2  38412  ltrniotavalbN  38607  trljco  38763  cdlemh  38840  cdlemk40t  38941  cdlemk40f  38942  cdleml9  39007  dihmeetlem3N  39328  dochkrshp  39409  dihprrn  39449  dihjat1  39452  dvh3dim  39469  dochkrsm  39481  dochexmid  39491  lcfl7lem  39522  lcfl9a  39528  lclkrlem1  39529  mapdspex  39691  mapdindp2  39744  mapdh6dN  39762  hdmap1l6d  39836  hdmap11lem2  39865  hdmap14lem4a  39894  hdmapip0  39938  hlhilset  39957  nnadd1com  40306  sn-negex12  40407  prjspner1  40472  0prjspnrel  40473  jm2.26a  40831  mnringmulrcld  41828  radcnvrat  41914  sumsnd  42551  icccncfext  43410  fperdvper  43442  dvcosax  43449  ioodvbdlimc1lem1  43454  ioodvbdlimc1lem2  43455  ioodvbdlimc2lem  43457  volioc  43495  itgiccshift  43503  stoweidlem34  43557  dirkercncflem2  43627  fourierdlem32  43662  fourierdlem41  43671  fourierdlem48  43677  fourierdlem64  43693  fourierdlem73  43702  fourierdlem79  43708  fourierdlem82  43711  fourierdlem97  43726  fourierdlem101  43730  fourierdlem109  43738  fourierdlem111  43740  fouriersw  43754  elaa2  43757  etransclem24  43781  etransclem25  43782  etransclem46  43803  nnfoctbdjlem  43975  ismeannd  43987  ndfatafv2undef  44683  fzopredsuc  44794  prproropf1olem3  44936  prproropf1olem4  44937  fmtnorec2lem  44973  2pwp1prmfmtno  45021  sfprmdvdsmersenne  45034  sgprmdvdsmersenne  45035  lighneallem2  45037  lighneallem3  45038  dfodd6  45068  dfeven4  45069  m1expevenALTV  45078  isomushgr  45257  isomuspgrlem2d  45262  clintopval  45377  lmod0rng  45405  zlidlring  45465  2zrngagrp  45480  rngcval  45499  ringcval  45545  dmmpossx2  45651  zlmodzxzscm  45672  zlmodzxzadd  45673  domnmsuppn0  45684  rmsuppss  45685  scmsuppss  45687  ply1mulgsumlem4  45709  ldepsprlem  45792  lincresunit2  45798  m1modmmod  45846  nn0sumshdiglemB  45945  2arymptfv  45975  ackval42  46021  affinecomb1  46027  itschlc0yqe  46085  itsclquadb  46101  2itscp  46106  0setrec  46388