Theorem sylan9eqr 2818

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  sbcied2  3786  csbied2  3887  opthhausdorff0  5484  fun2ssres  6561  fcoi1  6733  fcoi2  6734  funssfv  6883  fvtp1  7174  nvof1o  7259  onuninsuci  7815  ot1stg  7979  ot2ndg  7980  el2xptp0  8012  mpomptsx  8040  dmmpossx  8042  fmpox  8043  2ndconst  8074  offsplitfpar  8092  mpoxopoveq  8193  rdgeq12  8378  rdgsucmptnf  8394  frsucmptn  8404  oev2  8486  oesuclem  8488  oawordeulem  8517  om00  8538  omass  8543  omeulem1  8545  oeoa  8561  oeoe  8563  nnmass  8588  oaabs2  8613  omabs  8615  mapsnend  9011  omxpenlem  9044  sbthlem4  9056  sbthlem6  9058  fodomr  9094  ssenen  9117  fodomfir  9266  fi0  9360  cantnfp1  9630  cnfcomlem  9648  ttrclselem2  9675  cardaleph  10039  cflim2  10214  axdc4lem  10406  fpwwe2lem11  10593  fpwwe2lem12  10594  rankcf  10729  inatsk  10730  ltrnq  10931  addclprlem1  10968  mulclprlem  10971  1idpr  10981  prlem936  10999  reclem3pr  11001  mulcmpblnrlem  11022  recexsrlem  11055  map2psrpr  11062  addid0  11600  subdivcomb2  11881  nnadd1com  12230  nnnn0addcl  12505  zindd  12668  qaddcl  12960  qmulcl  12962  qreccl  12964  xaddnemnf  13233  xaddnepnf  13234  xaddcom  13237  xnegdi  13245  xaddass  13246  xpncan  13248  xleadd1a  13250  xlt2add  13257  rexmul  13268  xmulgt0  13280  xmulge0  13281  xmulasslem3  13283  xlemul1a  13285  xadddilem  13291  xadddi2  13294  modmuladd  13920  modm1p1mod0  13929  modfzo0difsn  13950  seqf1olem2  14049  expp1  14075  expneg  14076  expcllem  14079  mulexp  14108  expmul  14114  sqoddm1div8  14250  bcpasc  14328  hashrabsn01  14380  fseq1hash  14383  hashinfxadd  14392  hashfzo  14436  fnfz0hash  14453  ffzo0hash  14456  hashf1lem1  14462  hashge2el2dif  14487  hash3tpexb  14501  hashdifsnp1  14513  lsw0  14572  ccatval1  14584  ccatval2  14585  swrdval  14651  ccatopth  14723  reuccatpfxs1  14754  splval  14758  repswswrd  14791  2cshwcshw  14832  s4dom  14926  wrdlen2i  14949  shftfn  15080  reim0b  15137  cjexp  15168  sqeqd  15184  fsumser  15748  sumsnf  15761  binomlem  15850  expcnv  15885  prodsn  15983  prodsnf  15985  bpolylem  16069  bpoly2  16078  bpoly3  16079  ef0lem  16099  dvdsnegb  16298  mod2eq1n2dvds  16372  m1expe  16399  m1expo  16400  m1exp1  16401  flodddiv4  16440  sadadd2lem2  16475  bezoutr1  16594  dvdslcm  16623  lcmeq0  16625  lcmcl  16626  lcmabs  16630  lcmgcdlem  16631  lcmdvds  16633  lcmf0val  16647  lcmftp  16661  lcmfunsnlem2  16665  mulgcddvds  16680  divgcdcoprmex  16691  pcge0  16889  pcadd  16916  pcmpt2  16920  prmreclem4  16946  ramval  17035  ramcl  17056  fvprmselelfz  17071  fvprmselgcd1  17072  ressid2  17261  ressval2  17262  mndind  18853  frmdval  18876  efmnd  18895  smndex1igid  18931  smndex1igidOLD  18932  smndex1n0mnd  18940  mgm2nsgrplem3  18948  mulgfval  19102  mulgfvalALT  19103  mulgnn0subcl  19120  mulgnn0z  19134  cycsubm  19234  f1ghm0to0  19276  isga  19322  symgextfve  19450  symgfixf1  19468  f1omvdco2  19479  psgnsn  19551  odid  19569  gexid  19612  efgsval2  19764  frgpuptinv  19802  frgpup2  19807  dprdsn  20069  srgmulgass  20254  srgpcomp  20255  srgbinomlem4  20266  ringinvnzdiv  20338  rngcval  20655  ringcval  20684  isabvd  20849  issrng  20881  lmodvsmmulgdi  20952  mptscmfsupp0  20982  lvecinv  21171  lspdisj2  21185  lspfixed  21186  lspexch  21187  sralem  21231  srasca  21235  sravsca  21236  sraip  21237  znval  21575  psgndiflemB  21640  isphl  21668  assamulgscmlem2  21940  mplval  22028  opsrval  22087  psdmvr  22222  cply1mul  22347  gsummoncoe1  22359  evl1fval  22379  scmate  22558  scmatscm  22561  mdetdiagid  22648  mdetunilem7  22666  mdetuni0  22669  gsummatr01lem3  22705  gsummatr01lem4  22706  gsummatr01  22707  slesolinvbi  22729  cpmatacl  22764  cpmatinvcl  22765  pmatcollpw2lem  22825  monmatcollpw  22827  pmatcollpwfi  22830  mp2pm2mplem4  22857  pm2mp  22873  cpmadugsumlemF  22924  cpmadugsumfi  22925  cpmadumatpoly  22931  cayhamlem4  22936  cayleyhamilton0  22937  cayleyhamiltonALT  22939  indistopon  23049  0ntr  23119  pnrmopn  23391  reftr  23562  kgenval  23583  pt1hmeo  23854  fmval  23991  fmf  23993  istmd  24122  istgp  24125  tsmsval2  24178  isxmet2d  24375  xpsxmetlem  24427  xpsmet  24430  blfvalps  24431  tmsval  24529  isnlm  24723  nmoleub  24779  idnghm  24791  blssioo  24843  blcvx  24846  icccvx  25000  pcorevlem  25076  isclm  25114  caufval  25325  iscms  25395  mbfsup  25714  i1f1  25740  dvexp3  26028  rolle  26040  dvivth  26060  deg1add  26151  0dgr  26293  coefv0  26296  elqaalem2  26372  dvradcnv  26472  abelthlem8  26490  efper  26532  logtayl  26713  abscxpbnd  26806  relogbcxpb  26840  logbgcd1irr  26847  dcubic2  26897  rlimcnp2  27019  cvxcl  27037  zetacvg  27067  lgamgulmlem2  27082  vmaval  27165  chtub  27264  logexprlim  27277  dchrsum2  27320  sumdchr2  27322  bposlem2  27337  lgsdir  27384  lgsne0  27387  lgsdirnn0  27396  lgsdinn0  27397  lgsquadlem2  27433  2lgslem3a  27448  2lgslem3b  27449  2lgslem3c  27450  2lgslem3d  27451  2lgslem3a1  27452  2lgslem3b1  27453  2lgslem3c1  27454  2lgslem3d1  27455  2sqn0  27486  dchrvmasum2if  27549  dchrvmasumiflem1  27553  rpvmasum2  27564  pntpbnd1  27638  ostth2lem4  27688  expsp1  28510  trgcgrg  28672  tgcgr4  28688  ax5seglem1  29086  ax5seglem2  29087  ax5seglem5  29091  usgr1vr  29413  cplgr2vpr  29591  cplgr3v  29593  cusgrrusgr  29739  wlklenvm1  29779  wlk0prc  29810  wlksoneq1eq2  29820  crctcshwlkn0lem4  29970  crctcshwlkn0lem5  29971  crctcshwlkn0lem6  29972  crctcshlem4  29977  crctcsh  29981  wlkiswwlks1  30024  wwlksnext  30050  wwlksnextbi  30051  wwlksnextwrd  30054  midwwlks2s3  30109  clwlkclwwlklem2fv1  30154  clwlkclwwlklem2a4  30156  clwlkclwwlklem3  30160  clwwisshclwws  30174  erclwwlkeqlen  30178  clwwlkinwwlk  30199  clwwlkn2  30203  clwwlkf  30206  clwwlkf1  30208  eleclclwwlknlem2  30220  erclwwlkneqlen  30227  umgrhashecclwwlk  30237  eucrctshift  30402  eucrct2eupth  30404  fusgr2wsp2nb  30493  grpoidinvlem2  30665  vcz  30735  nvz  30829  lnon0  30958  ipasslem2  30992  htthlem  31077  hvpncan  31199  hiidge0  31258  normgt0  31287  hsn0elch  31408  shsel3  31475  spansneleq  31730  normcan  31736  h1datomi  31741  fh1  31778  spansncvi  31812  5oalem1  31814  5oalem3  31816  5oalem5  31818  3oalem2  31823  pjdsi  31872  kbpj  32116  0hmop  32143  0lnfn  32145  adj0  32154  nlelshi  32220  branmfn  32265  opsqrlem1  32300  hst1h  32387  mdsl0  32470  superpos  32514  sumdmdlem  32578  cdj3lem1  32594  f1od2  32882  xrpxdivcld  33073  xrge0npcan  33159  elrgspnlem2  33385  rlocf1  33416  resvid2  33477  resvval2  33478  qsdrng  33646  r1pquslmic  33768  0mplrim  33772  selvply1rhmlemb  33777  selvply1rhmlem2  33779  selvply1rhmlem4  33781  mplvrpmmhm  33804  mplvrpmrhm  33805  esplyfval0  33822  esplyfvaln  33832  vietalem  33837  rtelextdg2lem  33984  esumsnf  34322  esummulc1  34339  measxun2  34468  omsmeas  34581  sibfof  34598  probun  34677  signstfvn  34824  bnj517  35141  pthhashvtx  35439  ex-sategoelel  35732  mrsubfval  35819  msrval  35849  dfrdg2  36104  itgeq12i  36527  bj-prmoore  37566  bj-bary1lem1  37764  rdgeqoa  37825  finxpreclem2  37845  finxpreclem3  37848  matunitlindflem1  38076  poimirlem1  38081  poimirlem2  38082  poimirlem3  38083  poimirlem4  38084  poimirlem5  38085  poimirlem6  38086  poimirlem7  38087  poimirlem10  38090  poimirlem11  38091  poimirlem12  38092  poimirlem14  38094  poimirlem15  38095  poimirlem17  38097  poimirlem20  38100  poimirlem22  38102  poimirlem23  38103  poimirlem24  38104  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  mblfinlem2  38118  mblfinlem3  38119  ismblfin  38121  mbfposadd  38127  itg2addnclem  38131  itg2addnclem3  38133  itg2addnc  38134  ftc1anclem8  38160  areacirc  38173  ismtyval  38260  ismrer1  38298  grposnOLD  38342  rabeq12f  38617  csbeq12  38618  iuneq12f  38623  lsatcv1  39633  glbconN  39962  atltcvr  40020  3dim2  40053  islln2a  40102  2at0mat0  40110  islpln2a  40133  islvol2aN  40177  pmodlem2  40432  pmapjat1  40438  pcl0bN  40508  osumclN  40552  pexmidALTN  40563  lhp2at0nle  40620  4atexlemunv  40651  cdleme18b  40877  cdleme31sn1  40966  cdleme31sde  40970  cdleme31sn2  40974  ltrniotavalbN  41169  trljco  41325  cdlemh  41402  cdlemk40t  41503  cdlemk40f  41504  cdleml9  41569  dihmeetlem3N  41890  dochkrshp  41971  dihprrn  42011  dihjat1  42014  dvh3dim  42031  dochkrsm  42043  dochexmid  42053  lcfl7lem  42084  lcfl9a  42090  lclkrlem1  42091  mapdspex  42253  mapdindp2  42306  mapdh6dN  42324  hdmap1l6d  42398  hdmap11lem2  42427  hdmap14lem4a  42456  hdmapip0  42500  hlhilset  42519  mulgt0b2d  43061  fiabv  43115  prjspner1  43169  0prjspnrel  43170  jm2.26a  43538  onov0suclim  43812  oe0suclim  43815  cantnfresb  43862  onmcl  43869  omcl2  43871  tfsconcatun  43875  naddwordnexlem4  43939  mnringmulrcld  44765  radcnvrat  44851  sumsnd  45567  icccncfext  46422  fperdvper  46454  dvcosax  46461  ioodvbdlimc1lem1  46466  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  volioc  46507  itgiccshift  46515  stoweidlem34  46569  dirkercncflem2  46639  fourierdlem32  46674  fourierdlem41  46683  fourierdlem48  46689  fourierdlem64  46705  fourierdlem73  46714  fourierdlem79  46720  fourierdlem82  46723  fourierdlem97  46738  fourierdlem101  46742  fourierdlem109  46750  fourierdlem111  46752  fouriersw  46766  elaa2  46769  etransclem24  46793  etransclem25  46794  etransclem46  46815  nnfoctbdjlem  46990  ismeannd  47002  smfpimltxr  47282  smfpimgtxr  47315  ndfatafv2undef  47767  fzopredsuc  47879  m1modmmod  47919  modlt0b  47924  prproropf1olem3  48072  prproropf1olem4  48073  fmtnorec2lem  48112  2pwp1prmfmtno  48160  sfprmdvdsmersenne  48173  sgprmdvdsmersenne  48174  lighneallem2  48176  lighneallem3  48177  ppivalnnprm  48195  ppivalnnnprmge6  48196  dfodd6  48220  dfeven4  48221  m1expevenALTV  48230  isubgredg  48449  upgrimwlklem5  48484  gricushgr  48500  stgrusgra  48542  isubgr3stgrlem8  48556  clintopval  48787  lmod0rng  48812  zlidlring  48817  2zrngagrp  48832  dmmpossx2  48920  zlmodzxzscm  48940  zlmodzxzadd  48941  domnmsuppn0  48952  rmsuppss  48953  scmsuppss  48954  ply1mulgsumlem4  48972  ldepsprlem  49055  lincresunit2  49061  nn0sumshdiglemB  49203  2arymptfv  49233  ackval42  49279  affinecomb1  49285  itschlc0yqe  49343  itsclquadb  49359  2itscp  49364  incat  50183  0setrec  50286