Theorem sylan9eqr 2826

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  sbcied2  3797  csbied2  3898  opthhausdorff0  5499  fun2ssres  6579  fcoi1  6750  fcoi2  6751  funssfv  6900  fvtp1  7191  nvof1o  7276  onuninsuci  7832  ot1stg  7996  ot2ndg  7997  el2xptp0  8029  mpomptsx  8057  dmmpossx  8059  fmpox  8060  2ndconst  8092  offsplitfpar  8110  mpoxopoveq  8211  rdgeq12  8396  rdgsucmptnf  8412  frsucmptn  8422  oev2  8504  oesuclem  8506  oawordeulem  8535  om00  8556  omass  8561  omeulem1  8563  oeoa  8579  oeoe  8581  nnmass  8606  oaabs2  8631  omabs  8633  mapsnend  9029  omxpenlem  9062  sbthlem4  9074  sbthlem6  9076  fodomr  9112  ssenen  9135  fodomfir  9283  fi0  9376  cantnfp1  9646  cnfcomlem  9664  ttrclselem2  9691  cardaleph  10069  cflim2  10243  axdc4lem  10435  fpwwe2lem11  10622  fpwwe2lem12  10623  rankcf  10758  inatsk  10759  ltrnq  10960  addclprlem1  10997  mulclprlem  11000  1idpr  11010  prlem936  11028  reclem3pr  11030  mulcmpblnrlem  11051  recexsrlem  11084  map2psrpr  11091  addid0  11629  subdivcomb2  11907  nnadd1com  12255  nnnn0addcl  12530  zindd  12693  qaddcl  12985  qmulcl  12987  qreccl  12989  xaddnemnf  13258  xaddnepnf  13259  xaddcom  13262  xnegdi  13270  xaddass  13271  xpncan  13273  xleadd1a  13275  xlt2add  13282  rexmul  13293  xmulgt0  13305  xmulge0  13306  xmulasslem3  13308  xlemul1a  13310  xadddilem  13316  xadddi2  13319  modmuladd  13945  modm1p1mod0  13954  modfzo0difsn  13975  seqf1olem2  14074  expp1  14100  expneg  14101  expcllem  14104  mulexp  14133  expmul  14139  sqoddm1div8  14275  bcpasc  14353  hashrabsn01  14405  fseq1hash  14408  hashinfxadd  14417  hashfzo  14462  fnfz0hash  14479  ffzo0hash  14482  hashf1lem1  14488  hashge2el2dif  14513  hash3tpexb  14527  hashdifsnp1  14539  lsw0  14598  ccatval1  14610  ccatval2  14611  swrdval  14677  ccatopth  14749  reuccatpfxs1  14780  splval  14784  repswswrd  14817  2cshwcshw  14858  s4dom  14952  wrdlen2i  14975  shftfn  15106  reim0b  15166  cjexp  15197  sqeqd  15213  fsumser  15777  sumsnf  15790  binomlem  15879  expcnv  15914  prodsn  16012  prodsnf  16014  bpolylem  16098  bpoly2  16107  bpoly3  16108  ef0lem  16128  dvdsnegb  16327  mod2eq1n2dvds  16401  m1expe  16428  m1expo  16429  m1exp1  16430  flodddiv4  16469  sadadd2lem2  16504  bezoutr1  16623  dvdslcm  16652  lcmeq0  16654  lcmcl  16655  lcmabs  16659  lcmgcdlem  16660  lcmdvds  16662  lcmf0val  16676  lcmftp  16690  lcmfunsnlem2  16694  mulgcddvds  16709  divgcdcoprmex  16720  pcge0  16918  pcadd  16945  pcmpt2  16949  prmreclem4  16975  ramval  17064  ramcl  17085  fvprmselelfz  17100  fvprmselgcd1  17101  ressid2  17290  ressval2  17291  mndind  18883  frmdval  18906  efmnd  18925  smndex1igid  18961  smndex1igidOLD  18962  smndex1n0mnd  18970  mgm2nsgrplem3  18978  mulgfval  19131  mulgfvalALT  19132  mulgnn0subcl  19149  mulgnn0z  19163  cycsubm  19269  f1ghm0to0  19311  isga  19357  symgextfve  19485  symgfixf1  19503  f1omvdco2  19514  psgnsn  19586  odid  19604  gexid  19647  efgsval2  19799  frgpuptinv  19837  frgpup2  19842  dprdsn  20104  srgmulgass  20295  srgpcomp  20296  srgbinomlem4  20307  ringinvnzdiv  20380  rngcval  20699  ringcval  20728  isabvd  20889  issrng  20921  lmodvsmmulgdi  20992  mptscmfsupp0  21022  lvecinv  21211  lspdisj2  21225  lspfixed  21226  lspexch  21227  sralem  21271  srasca  21275  sravsca  21276  sraip  21277  znval  21650  psgndiflemB  21715  isphl  21743  assamulgscmlem2  22015  mplval  22103  opsrval  22162  psdmvr  22297  cply1mul  22421  gsummoncoe1  22433  evl1fval  22453  scmate  22632  scmatscm  22635  mdetdiagid  22722  mdetunilem7  22740  mdetuni0  22743  gsummatr01lem3  22779  gsummatr01lem4  22780  gsummatr01  22781  slesolinvbi  22803  cpmatacl  22838  cpmatinvcl  22839  pmatcollpw2lem  22899  monmatcollpw  22901  pmatcollpwfi  22904  mp2pm2mplem4  22931  pm2mp  22947  cpmadugsumlemF  22998  cpmadugsumfi  22999  cpmadumatpoly  23005  cayhamlem4  23010  cayleyhamilton0  23011  cayleyhamiltonALT  23013  indistopon  23123  0ntr  23193  pnrmopn  23465  reftr  23636  kgenval  23657  pt1hmeo  23928  fmval  24065  fmf  24067  istmd  24196  istgp  24199  tsmsval2  24252  isxmet2d  24449  xpsxmetlem  24501  xpsmet  24504  blfvalps  24505  tmsval  24603  isnlm  24797  nmoleub  24853  idnghm  24865  blssioo  24917  blcvx  24920  icccvx  25074  pcorevlem  25150  isclm  25188  caufval  25399  iscms  25469  mbfsup  25788  i1f1  25814  dvexp3  26102  rolle  26114  dvivth  26134  deg1add  26225  0dgr  26367  coefv0  26370  elqaalem2  26446  dvradcnv  26546  abelthlem8  26564  efper  26606  logtayl  26787  abscxpbnd  26880  relogbcxpb  26914  logbgcd1irr  26921  dcubic2  26971  rlimcnp2  27093  cvxcl  27111  zetacvg  27141  lgamgulmlem2  27156  vmaval  27239  chtub  27338  logexprlim  27351  dchrsum2  27394  sumdchr2  27396  bposlem2  27411  lgsdir  27458  lgsne0  27461  lgsdirnn0  27470  lgsdinn0  27471  lgsquadlem2  27507  2lgslem3a  27522  2lgslem3b  27523  2lgslem3c  27524  2lgslem3d  27525  2lgslem3a1  27526  2lgslem3b1  27527  2lgslem3c1  27528  2lgslem3d1  27529  2sqn0  27560  dchrvmasum2if  27623  dchrvmasumiflem1  27627  rpvmasum2  27638  pntpbnd1  27712  ostth2lem4  27762  expsp1  28584  trgcgrg  28746  tgcgr4  28762  ax5seglem1  29215  ax5seglem2  29216  ax5seglem5  29220  usgr1vr  29542  cplgr2vpr  29720  cplgr3v  29722  cusgrrusgr  29868  wlklenvm1  29908  wlk0prc  29939  wlksoneq1eq2  29949  crctcshwlkn0lem4  30099  crctcshwlkn0lem5  30100  crctcshwlkn0lem6  30101  crctcshlem4  30106  crctcsh  30110  wlkiswwlks1  30153  wwlksnext  30179  wwlksnextbi  30180  wwlksnextwrd  30183  midwwlks2s3  30238  clwlkclwwlklem2fv1  30283  clwlkclwwlklem2a4  30285  clwlkclwwlklem3  30289  clwwisshclwws  30303  erclwwlkeqlen  30307  clwwlkinwwlk  30328  clwwlkn2  30332  clwwlkf  30335  clwwlkf1  30337  eleclclwwlknlem2  30349  erclwwlkneqlen  30356  umgrhashecclwwlk  30366  eucrctshift  30531  eucrct2eupth  30533  fusgr2wsp2nb  30622  grpoidinvlem2  30794  vcz  30864  nvz  30958  lnon0  31087  ipasslem2  31121  htthlem  31206  hvpncan  31328  hiidge0  31387  normgt0  31416  hsn0elch  31537  shsel3  31604  spansneleq  31859  normcan  31865  h1datomi  31870  fh1  31907  spansncvi  31941  5oalem1  31943  5oalem3  31945  5oalem5  31947  3oalem2  31952  pjdsi  32001  kbpj  32245  0hmop  32272  0lnfn  32274  adj0  32283  nlelshi  32349  branmfn  32394  opsqrlem1  32429  hst1h  32516  mdsl0  32599  superpos  32643  sumdmdlem  32707  cdj3lem1  32723  f1od2  33001  xrpxdivcld  33191  xrge0npcan  33277  elrgspnlem2  33500  rlocf1  33531  resvid2  33589  resvval2  33590  qsdrng  33720  r1pquslmic  33841  0mplrim  33845  selvply1rhmlemb  33850  selvply1rhmlem2  33852  selvply1rhmlem4  33854  mplvrpmmhm  33877  mplvrpmrhm  33878  esplyfval0  33895  esplyfvaln  33905  vietalem  33910  rtelextdg2lem  34057  esumsnf  34395  esummulc1  34412  measxun2  34541  omsmeas  34654  sibfof  34671  probun  34750  signstfvn  34897  bnj517  35214  pthhashvtx  35515  ex-sategoelel  35808  mrsubfval  35895  msrval  35925  dfrdg2  36180  itgeq12i  36603  bj-prmoore  37640  bj-bary1lem1  37838  rdgeqoa  37899  finxpreclem2  37919  finxpreclem3  37922  matunitlindflem1  38150  poimirlem1  38155  poimirlem2  38156  poimirlem3  38157  poimirlem4  38158  poimirlem5  38159  poimirlem6  38160  poimirlem7  38161  poimirlem10  38164  poimirlem11  38165  poimirlem12  38166  poimirlem14  38168  poimirlem15  38169  poimirlem17  38171  poimirlem20  38174  poimirlem22  38176  poimirlem23  38177  poimirlem24  38178  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  mblfinlem2  38192  mblfinlem3  38193  ismblfin  38195  mbfposadd  38201  itg2addnclem  38205  itg2addnclem3  38207  itg2addnc  38208  ftc1anclem8  38234  areacirc  38247  ismtyval  38334  ismrer1  38372  grposnOLD  38416  rabeq12f  38691  csbeq12  38692  iuneq12f  38697  lsatcv1  39707  glbconN  40036  atltcvr  40094  3dim2  40127  islln2a  40176  2at0mat0  40184  islpln2a  40207  islvol2aN  40251  pmodlem2  40506  pmapjat1  40512  pcl0bN  40582  osumclN  40626  pexmidALTN  40637  lhp2at0nle  40694  4atexlemunv  40725  cdleme18b  40951  cdleme31sn1  41040  cdleme31sde  41044  cdleme31sn2  41048  ltrniotavalbN  41243  trljco  41399  cdlemh  41476  cdlemk40t  41577  cdlemk40f  41578  cdleml9  41643  dihmeetlem3N  41964  dochkrshp  42045  dihprrn  42085  dihjat1  42088  dvh3dim  42105  dochkrsm  42117  dochexmid  42127  lcfl7lem  42158  lcfl9a  42164  lclkrlem1  42165  mapdspex  42327  mapdindp2  42380  mapdh6dN  42398  hdmap1l6d  42472  hdmap11lem2  42501  hdmap14lem4a  42530  hdmapip0  42574  hlhilset  42593  mulgt0b2d  43137  fiabv  43191  prjspner1  43245  0prjspnrel  43246  jm2.26a  43614  onov0suclim  43888  oe0suclim  43891  cantnfresb  43938  onmcl  43945  omcl2  43947  tfsconcatun  43951  naddwordnexlem4  44015  mnringmulrcld  44839  radcnvrat  44911  sumsnd  45633  icccncfext  46488  fperdvper  46520  dvcosax  46527  ioodvbdlimc1lem1  46532  ioodvbdlimc1lem2  46533  ioodvbdlimc2lem  46535  volioc  46573  itgiccshift  46581  stoweidlem34  46635  dirkercncflem2  46705  fourierdlem32  46740  fourierdlem41  46749  fourierdlem48  46755  fourierdlem64  46771  fourierdlem73  46780  fourierdlem79  46786  fourierdlem82  46789  fourierdlem97  46804  fourierdlem101  46808  fourierdlem109  46816  fourierdlem111  46818  fouriersw  46832  elaa2  46835  etransclem24  46859  etransclem25  46860  etransclem46  46881  nnfoctbdjlem  47056  ismeannd  47068  smfpimltxr  47348  smfpimgtxr  47381  ndfatafv2undef  47833  fzopredsuc  47945  m1modmmod  47985  modlt0b  47990  prproropf1olem3  48138  prproropf1olem4  48139  fmtnorec2lem  48178  2pwp1prmfmtno  48226  sfprmdvdsmersenne  48239  sgprmdvdsmersenne  48240  lighneallem2  48242  lighneallem3  48243  ppivalnnprm  48261  ppivalnnnprmge6  48262  dfodd6  48286  dfeven4  48287  m1expevenALTV  48296  isubgredg  48515  upgrimwlklem5  48550  gricushgr  48566  stgrusgra  48608  isubgr3stgrlem8  48622  clintopval  48853  lmod0rng  48878  zlidlring  48883  2zrngagrp  48898  dmmpossx2  48997  zlmodzxzscm  49017  zlmodzxzadd  49018  domnmsuppn0  49029  rmsuppss  49030  scmsuppss  49031  ply1mulgsumlem4  49049  ldepsprlem  49132  lincresunit2  49138  nn0sumshdiglemB  49280  2arymptfv  49310  ackval42  49356  affinecomb1  49362  itschlc0yqe  49420  itsclquadb  49436  2itscp  49441  incat  50259  0setrec  50362