Theorem sylan9eqr 2817

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  sbcied2  3782  csbied2  3884  opthhausdorff0  5490  fun2ssres  6588  fcoi1  6759  fcoi2  6760  funssfv  6909  fvtp1  7202  nvof1o  7290  onuninsuci  7853  ot1stg  8017  ot2ndg  8018  el2xptp0  8049  mpomptsx  8077  dmmpossx  8079  fmpox  8080  f1od2  8112  2ndconst  8116  offsplitfpar  8134  mpoxopoveq  8241  rdgeq12  8426  rdgsucmptnf  8442  frsucmptn  8452  oev2  8536  oesuclem  8538  oawordeulem  8567  om00  8588  omass  8593  omeulem1  8595  oeoa  8611  oeoe  8613  nnmass  8638  oaabs2  8663  omabs  8665  mapsnend  9069  omxpenlem  9102  sbthlem4  9114  sbthlem6  9116  fodomr  9152  ssenen  9175  fodomfir  9324  fi0  9417  cantnfp1  9687  cnfcomlem  9705  ttrclselem2  9732  cardaleph  10173  cflim2  10346  axdc4lem  10538  fpwwe2lem11  10731  fpwwe2lem12  10732  rankcf  10867  inatsk  10868  ltrnq  11069  addclprlem1  11106  mulclprlem  11109  1idpr  11119  prlem936  11137  reclem3pr  11139  mulcmpblnrlem  11160  recexsrlem  11193  map2psrpr  11200  addid0  11740  subdivcomb2  12018  nnadd1com  12366  nnnn0addcl  12641  zindd  12805  qaddcl  13098  qmulcl  13100  qreccl  13102  xaddnemnf  13371  xaddnepnf  13372  xaddcom  13375  xnegdi  13383  xaddass  13384  xpncan  13386  xleadd1a  13388  xlt2add  13395  rexmul  13406  xmulgt0  13418  xmulge0  13419  xmulasslem3  13421  xlemul1a  13423  xadddilem  13429  xadddi2  13432  modmuladd  14061  modm1p1mod0  14070  modfzo0difsn  14091  seqf1olem2  14190  expp1  14216  expneg  14217  expcllem  14220  mulexp  14249  expmul  14255  sqoddm1div8  14392  bcpasc  14470  hashrabsn01  14522  fseq1hash  14525  hashinfxadd  14534  hashfzo  14579  fnfz0hash  14596  ffzo0hash  14599  hashf1lem1  14605  hashge2el2dif  14630  hash3tpexb  14644  hashdifsnp1  14656  lsw0  14715  ccatval1  14727  ccatval2  14728  swrdval  14797  ccatopth  14871  reuccatpfxs1  14902  splval  14906  repswswrd  14941  2cshwcshw  14982  s4dom  15077  wrdlen2i  15100  shftfn  15233  reim0b  15293  cjexp  15324  sqeqd  15340  fsumser  15903  sumsnf  15916  binomlem  16005  expcnv  16040  prodsn  16136  prodsnf  16138  bpolylem  16221  bpoly2  16230  bpoly3  16231  ef0lem  16251  dvdsnegb  16450  mod2eq1n2dvds  16524  m1expe  16551  m1expo  16552  m1exp1  16553  flodddiv4  16592  sadadd2lem2  16627  bezoutr1  16751  dvdslcm  16780  lcmeq0  16782  lcmcl  16783  lcmabs  16787  lcmgcdlem  16788  lcmdvds  16790  lcmf0val  16804  lcmftp  16818  lcmfunsnlem2  16822  mulgcddvds  16837  divgcdcoprmex  16848  pcge0  17047  pcadd  17074  pcmpt2  17078  prmreclem4  17104  ramval  17193  ramcl  17214  fvprmselelfz  17229  fvprmselgcd1  17230  ressid2  17419  ressval2  17420  mndind  19031  frmdval  19054  efmnd  19073  smndex1igid  19109  smndex1igidOLD  19110  smndex1n0mnd  19118  mgm2nsgrplem3  19126  mulgfval  19286  mulgfvalALT  19287  mulgnn0subcl  19304  mulgnn0z  19318  cycsubm  19424  f1ghm0to0  19466  isga  19512  symgextfve  19640  symgfixf1  19658  f1omvdco2  19669  psgnsn  19741  odid  19759  gexid  19802  efgsval2  19954  frgpuptinv  19992  frgpup2  19997  dprdsn  20259  srgmulgass  20450  srgpcomp  20451  srgbinomlem4  20462  ringinvnzdiv  20539  rngcval  20877  ringcval  20906  isabvd  21076  issrng  21108  lmodvsmmulgdi  21179  mptscmfsupp0  21209  lvecinv  21398  lspdisj2  21412  lspfixed  21413  lspexch  21414  sralem  21458  srasca  21462  sravsca  21463  sraip  21464  znval  21848  psgndiflemB  21913  isphl  21941  assamulgscmlem2  22215  mplval  22303  opsrval  22362  psdmvr  22497  cply1mul  22621  gsummoncoe1  22633  evl1fval  22653  scmate  22832  scmatscm  22835  mdetdiagid  22922  mdetunilem7  22940  mdetuni0  22943  gsummatr01lem3  22979  gsummatr01lem4  22980  gsummatr01  22981  matunitlindflem1  23001  slesolinvbi  23006  cpmatacl  23041  cpmatinvcl  23042  pmatcollpw2lem  23102  monmatcollpw  23104  pmatcollpwfi  23107  mp2pm2mplem4  23134  pm2mp  23150  cpmadugsumlemF  23201  cpmadugsumfi  23202  cpmadumatpoly  23208  cayhamlem4  23213  cayleyhamilton0  23214  cayleyhamiltonALT  23216  indistopon  23326  0ntr  23396  pnrmopn  23668  reftr  23840  kgenval  23861  pt1hmeo  24132  fmval  24269  fmf  24271  istmd  24400  istgp  24403  tsmsval2  24456  isxmet2d  24653  xpsxmetlem  24705  xpsmet  24708  blfvalps  24709  tmsval  24807  isnlm  25001  nmoleub  25057  idnghm  25069  blssioo  25121  blcvx  25124  icccvx  25278  pcorevlem  25354  isclm  25392  caufval  25603  iscms  25673  mbfsup  25992  i1f1  26018  dvexp3  26305  rolle  26317  dvivth  26337  deg1add  26428  0dgr  26571  coefv0  26574  elqaalem2  26650  dvradcnv  26755  abelthlem8  26773  efper  26815  logtayl  26995  abscxpbnd  27088  relogbcxpb  27122  logbgcd1irr  27129  dcubic2  27179  rlimcnp2  27301  cvxcl  27319  zetacvg  27349  lgamgulmlem2  27364  vmaval  27447  chtub  27546  logexprlim  27559  dchrsum2  27602  sumdchr2  27604  bposlem2  27619  lgsdir  27666  lgsne0  27669  lgsdirnn0  27678  lgsdinn0  27679  lgsquadlem2  27715  2lgslem3a  27730  2lgslem3b  27731  2lgslem3c  27732  2lgslem3d  27733  2lgslem3a1  27734  2lgslem3b1  27735  2lgslem3c1  27736  2lgslem3d1  27737  2sqn0  27768  dchrvmasum2if  27831  dchrvmasumiflem1  27835  rpvmasum2  27846  pntpbnd1  27920  ostth2lem4  27970  expsp1  28822  trgcgrg  28985  tgcgr4  29001  ax5seglem1  29513  ax5seglem2  29514  ax5seglem5  29518  usgr1vr  29843  cplgr2vpr  30021  cplgr3v  30023  cusgrrusgr  30169  wlklenvm1  30209  wlk0prc  30240  wlksoneq1eq2  30250  pthhashvtx  30322  crctcshwlkn0lem4  30409  crctcshwlkn0lem5  30410  crctcshwlkn0lem6  30411  crctcshlem4  30416  crctcsh  30420  wlkiswwlks1  30463  wwlksnext  30489  wwlksnextbi  30490  wwlksnextwrd  30493  midwwlks2s3  30548  clwlkclwwlklem2fv1  30593  clwlkclwwlklem2a4  30595  clwlkclwwlklem3  30599  clwwisshclwws  30613  erclwwlkeqlen  30617  clwwlkinwwlk  30638  clwwlkn2  30642  clwwlkf  30645  clwwlkf1  30647  eleclclwwlknlem2  30659  erclwwlkneqlen  30666  umgrhashecclwwlk  30676  eucrctshift  30851  eucrct2eupth  30853  fusgr2wsp2nb  30942  grpoidinvlem2  31114  vcz  31184  nvz  31278  lnon0  31407  ipasslem2  31441  htthlem  31526  hvpncan  31648  hiidge0  31707  normgt0  31736  hsn0elch  31857  shsel3  31924  spansneleq  32179  normcan  32185  h1datomi  32190  fh1  32227  spansncvi  32261  5oalem1  32263  5oalem3  32265  5oalem5  32267  3oalem2  32272  pjdsi  32321  kbpj  32565  0hmop  32592  0lnfn  32594  adj0  32603  nlelshi  32669  branmfn  32714  opsqrlem1  32749  hst1h  32836  mdsl0  32919  superpos  32963  sumdmdlem  33027  cdj3lem1  33043  xrpxdivcld  33549  xrge0npcan  33629  elrgspnlem2  33852  rlocf1  33883  resvid2  33939  resvval2  33940  qsdrng  34069  r1pquslmic  34190  0mplrim  34194  selvply1rhmlemb  34199  selvply1rhmlem2  34201  selvply1rhmlem4  34203  mplvrpmmhm  34226  mplvrpmrhm  34227  esplyfval0  34244  esplyfvaln  34254  vietalem  34259  rtelextdg2lem  34406  esumsnf  34744  esummulc1  34761  measxun2  34891  omsmeas  35003  sibfof  35020  probun  35099  signstfvn  35246  bnj517  35563  brlexod  35940  brr0d  35942  ex-sategoelel  36274  mrsubfval  36361  msrval  36391  dfrdg2  36651  itgeq12i  37089  mh-inf3f1  37423  bj-prmoore  38142  bj-bary1lem1  38339  rdgeqoa  38400  finxpreclem2  38420  finxpreclem3  38423  poimirlem1  38646  poimirlem2  38647  poimirlem3  38648  poimirlem4  38649  poimirlem5  38650  poimirlem6  38651  poimirlem7  38652  poimirlem10  38655  poimirlem11  38656  poimirlem12  38657  poimirlem14  38659  poimirlem15  38660  poimirlem17  38662  poimirlem20  38665  poimirlem22  38667  poimirlem23  38668  poimirlem24  38669  poimirlem25  38670  poimirlem26  38671  poimirlem27  38672  mblfinlem2  38683  mblfinlem3  38684  ismblfin  38686  mbfposadd  38692  itg2addnclem  38696  itg2addnclem3  38698  itg2addnc  38699  ftc1anclem8  38725  areacirc  38738  ismtyval  38841  ismrer1  38879  grposnOLD  38923  rabeq12f  39196  csbeq12  39197  iuneq12f  39202  lsatcv1  40212  glbconN  40541  atltcvr  40599  3dim2  40632  islln2a  40681  2at0mat0  40689  islpln2a  40712  islvol2aN  40756  pmodlem2  41011  pmapjat1  41017  pcl0bN  41087  osumclN  41131  pexmidALTN  41142  lhp2at0nle  41199  4atexlemunv  41230  cdleme18b  41456  cdleme31sn1  41545  cdleme31sde  41549  cdleme31sn2  41553  ltrniotavalbN  41748  trljco  41904  cdlemh  41981  cdlemk40t  42082  cdlemk40f  42083  cdleml9  42148  dihmeetlem3N  42469  dochkrshp  42550  dihprrn  42590  dihjat1  42593  dvh3dim  42610  dochkrsm  42622  dochexmid  42632  lcfl7lem  42663  lcfl9a  42669  lclkrlem1  42670  mapdspex  42832  mapdindp2  42885  mapdh6dN  42903  hdmap1l6d  42977  hdmap11lem2  43006  hdmap14lem4a  43035  hdmapip0  43079  hlhilset  43098  mulgt0b2d  43649  fiabv  43707  0prjspnrel  43770  jm2.26a  44114  onov0suclim  44383  oe0suclim  44386  cantnfresb  44433  onmcl  44440  omcl2  44442  tfsconcatun  44446  naddwordnexlem4  44510  mnringmulrcld  45333  radcnvrat  45405  sumsnd  46150  icccncfext  47004  fperdvper  47036  dvcosax  47043  ioodvbdlimc1lem1  47048  ioodvbdlimc1lem2  47049  ioodvbdlimc2lem  47051  volioc  47089  itgiccshift  47097  stoweidlem34  47151  dirkercncflem2  47221  fourierdlem32  47256  fourierdlem41  47265  fourierdlem48  47271  fourierdlem64  47287  fourierdlem73  47296  fourierdlem79  47302  fourierdlem82  47305  fourierdlem97  47320  fourierdlem101  47324  fourierdlem109  47332  fourierdlem111  47334  fouriersw  47348  elaa2  47351  etransclem24  47375  etransclem25  47376  etransclem46  47397  nnfoctbdjlem  47572  ismeannd  47584  smfpimltxr  47864  smfpimgtxr  47897  ndfatafv2undef  48389  fzopredsuc  48501  m1modmmod  48541  modlt0b  48546  prproropf1olem3  48694  prproropf1olem4  48695  fmtnorec2lem  48734  2pwp1prmfmtno  48782  sfprmdvdsmersenne  48795  sgprmdvdsmersenne  48796  lighneallem2  48798  lighneallem3  48799  ppivalnnprm  48817  ppivalnnnprmge6  48818  dfodd6  48842  dfeven4  48843  m1expevenALTV  48852  isubgredg  49071  upgrimwlklem5  49106  gricushgr  49122  stgrusgra  49164  isubgr3stgrlem8  49178  clintopval  49408  lmod0rng  49433  zlidlring  49438  2zrngagrp  49453  dmmpossx2  49556  zlmodzxzscm  49576  zlmodzxzadd  49577  domnmsuppn0  49588  rmsuppss  49589  scmsuppss  49590  ply1mulgsumlem4  49608  ldepsprlem  49691  lincresunit2  49697  nn0sumshdiglemB  49839  2arymptfv  49869  ackval42  49915  affinecomb1  49921  itschlc0yqe  49979  itsclquadb  49995  2itscp  50000  incat  50846  0setrec  50979