Theorem sylan9eqr 2820

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  sbcied2  3786  csbied2  3888  opthhausdorff0  5498  fun2ssres  6613  fcoi1  6786  fcoi2  6787  funssfv  6937  fvtp1  7231  nvof1o  7319  onuninsuci  7885  ot1stg  8049  ot2ndg  8050  el2xptp0  8081  mpomptsx  8110  dmmpossx  8112  fmpox  8113  f1od2  8145  2ndconst  8149  offsplitfpar  8167  mpoxopoveq  8274  rdgeq12  8459  rdgsucmptnf  8475  frsucmptn  8485  oev2  8569  oesuclem  8571  oawordeulem  8600  om00  8621  omass  8626  omeulem1  8628  oeoa  8644  oeoe  8646  nnmass  8671  oaabs2  8696  omabs  8698  mapsnend  9102  omxpenlem  9135  sbthlem4  9147  sbthlem6  9149  fodomr  9185  ssenen  9208  fodomfir  9357  fi0  9449  cantnfp1  9719  cnfcomlem  9737  ttrclselem2  9764  cardaleph  10207  cflim2  10380  axdc4lem  10572  fpwwe2lem11  10765  fpwwe2lem12  10766  rankcf  10901  inatsk  10902  ltrnq  11103  addclprlem1  11140  mulclprlem  11143  1idpr  11153  prlem936  11171  reclem3pr  11173  mulcmpblnrlem  11194  recexsrlem  11227  map2psrpr  11234  addid0  11774  subdivcomb2  12053  nnadd1com  12401  nnnn0addcl  12676  zindd  12840  qaddcl  13133  qmulcl  13135  qreccl  13137  xaddnemnf  13406  xaddnepnf  13407  xaddcom  13410  xnegdi  13418  xaddass  13419  xpncan  13421  xleadd1a  13423  xlt2add  13430  rexmul  13441  xmulgt0  13453  xmulge0  13454  xmulasslem3  13456  xlemul1a  13458  xadddilem  13464  xadddi2  13467  modmuladd  14096  modm1p1mod0  14105  modfzo0difsn  14126  seqf1olem2  14225  expp1  14251  expneg  14252  expcllem  14255  mulexp  14284  expmul  14290  sqoddm1div8  14428  bcpasc  14506  hashrabsn01  14558  fseq1hash  14561  hashinfxadd  14570  hashfzo  14615  fnfz0hash  14632  ffzo0hash  14635  hashf1lem1  14641  hashge2el2dif  14666  hash3tpexb  14680  hashdifsnp1  14692  lsw0  14751  ccatval1  14763  ccatval2  14764  swrdval  14833  ccatopth  14907  reuccatpfxs1  14938  splval  14942  repswswrd  14977  2cshwcshw  15018  s4dom  15113  wrdlen2i  15136  shftfn  15269  reim0b  15329  cjexp  15360  sqeqd  15376  fsumser  15940  sumsnf  15953  binomlem  16042  expcnv  16077  prodsn  16173  prodsnf  16175  bpolylem  16258  bpoly2  16267  bpoly3  16268  ef0lem  16288  dvdsnegb  16487  mod2eq1n2dvds  16561  m1expe  16588  m1expo  16589  m1exp1  16590  flodddiv4  16629  sadadd2lem2  16664  bezoutr1  16788  dvdslcm  16817  lcmeq0  16819  lcmcl  16820  lcmabs  16824  lcmgcdlem  16825  lcmdvds  16827  lcmf0val  16841  lcmftp  16855  lcmfunsnlem2  16859  mulgcddvds  16874  divgcdcoprmex  16885  pcge0  17084  pcadd  17111  pcmpt2  17115  prmreclem4  17141  ramval  17230  ramcl  17251  fvprmselelfz  17266  fvprmselgcd1  17267  ressid2  17456  ressval2  17457  mndind  19074  frmdval  19097  efmnd  19116  smndex1igid  19152  smndex1igidOLD  19153  smndex1n0mnd  19161  mgm2nsgrplem3  19169  mulgfval  19329  mulgfvalALT  19330  mulgnn0subcl  19347  mulgnn0z  19361  cycsubm  19467  f1ghm0to0  19509  isga  19556  symgextfve  19684  symgfixf1  19702  f1omvdco2  19713  psgnsn  19785  odid  19803  gexid  19846  efgsval2  19998  frgpuptinv  20036  frgpup2  20041  dprdsn  20303  srgmulgass  20494  srgpcomp  20495  srgbinomlem4  20506  ringinvnzdiv  20583  rngcval  20921  ringcval  20950  isabvd  21120  issrng  21152  lmodvsmmulgdi  21223  mptscmfsupp0  21253  lvecinv  21442  lspdisj2  21456  lspfixed  21457  lspexch  21458  sralem  21502  srasca  21506  sravsca  21507  sraip  21508  znval  21896  psgndiflemB  21961  isphl  21989  assamulgscmlem2  22263  mplval  22351  opsrval  22410  psdmvr  22545  cply1mul  22669  gsummoncoe1  22681  evl1fval  22701  scmate  22880  scmatscm  22883  mdetdiagid  22970  mdetunilem7  22988  mdetuni0  22991  gsummatr01lem3  23027  gsummatr01lem4  23028  gsummatr01  23029  matunitlindflem1  23049  slesolinvbi  23054  cpmatacl  23089  cpmatinvcl  23090  pmatcollpw2lem  23150  monmatcollpw  23152  pmatcollpwfi  23155  mp2pm2mplem4  23182  pm2mp  23198  cpmadugsumlemF  23249  cpmadugsumfi  23250  cpmadumatpoly  23256  cayhamlem4  23261  cayleyhamilton0  23262  cayleyhamiltonALT  23264  indistopon  23374  0ntr  23444  pnrmopn  23716  reftr  23888  kgenval  23909  pt1hmeo  24180  fmval  24317  fmf  24319  istmd  24448  istgp  24451  tsmsval2  24504  isxmet2d  24701  xpsxmetlem  24753  xpsmet  24756  blfvalps  24757  tmsval  24855  isnlm  25049  nmoleub  25105  idnghm  25117  blssioo  25169  blcvx  25172  icccvx  25326  pcorevlem  25402  isclm  25440  caufval  25651  iscms  25721  mbfsup  26040  i1f1  26066  dvexp3  26353  rolle  26365  dvivth  26385  deg1add  26476  0dgr  26619  coefv0  26622  elqaalem2  26700  dvradcnv  26805  abelthlem8  26823  efper  26865  logtayl  27045  abscxpbnd  27138  relogbcxpb  27172  logbgcd1irr  27179  dcubic2  27229  rlimcnp2  27351  cvxcl  27369  zetacvg  27399  lgamgulmlem2  27414  vmaval  27497  chtub  27596  logexprlim  27609  dchrsum2  27652  sumdchr2  27654  bposlem2  27669  lgsdir  27716  lgsne0  27719  lgsdirnn0  27728  lgsdinn0  27729  lgsquadlem2  27765  2lgslem3a  27780  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  2lgslem3a1  27784  2lgslem3b1  27785  2lgslem3c1  27786  2lgslem3d1  27787  2sqn0  27818  dchrvmasum2if  27881  dchrvmasumiflem1  27885  rpvmasum2  27896  pntpbnd1  27970  ostth2lem4  28020  expsp1  28872  trgcgrg  29035  tgcgr4  29051  ax5seglem1  29563  ax5seglem2  29564  ax5seglem5  29568  usgr1vr  29893  cplgr2vpr  30071  cplgr3v  30073  cusgrrusgr  30219  wlklenvm1  30259  wlk0prc  30290  wlksoneq1eq2  30300  pthhashvtx  30372  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  crctcshwlkn0lem6  30461  crctcshlem4  30466  crctcsh  30470  wlkiswwlks1  30513  wwlksnext  30539  wwlksnextbi  30540  wwlksnextwrd  30543  midwwlks2s3  30598  clwlkclwwlklem2fv1  30643  clwlkclwwlklem2a4  30645  clwlkclwwlklem3  30649  clwwisshclwws  30663  erclwwlkeqlen  30667  clwwlkinwwlk  30688  clwwlkn2  30692  clwwlkf  30695  clwwlkf1  30697  eleclclwwlknlem2  30709  erclwwlkneqlen  30716  umgrhashecclwwlk  30726  eucrctshift  30901  eucrct2eupth  30903  fusgr2wsp2nb  30992  grpoidinvlem2  31164  vcz  31234  nvz  31328  lnon0  31457  ipasslem2  31491  htthlem  31576  hvpncan  31698  hiidge0  31757  normgt0  31786  hsn0elch  31907  shsel3  31974  spansneleq  32229  normcan  32235  h1datomi  32240  fh1  32277  spansncvi  32311  5oalem1  32313  5oalem3  32315  5oalem5  32317  3oalem2  32322  pjdsi  32371  kbpj  32615  0hmop  32642  0lnfn  32644  adj0  32653  nlelshi  32719  branmfn  32764  opsqrlem1  32799  hst1h  32886  mdsl0  32969  superpos  33013  sumdmdlem  33077  cdj3lem1  33093  xrpxdivcld  33597  xrge0npcan  33680  elrgspnlem2  33903  rlocf1  33934  resvid2  33995  resvval2  33996  qsdrng  34125  r1pquslmic  34247  0mplrim  34257  selvply1rhmlemb  34262  selvply1rhmlem2  34264  selvply1rhmlem4  34266  mplvrpmmhm  34289  mplvrpmrhm  34290  esplyfval0  34307  esplyfvaln  34317  vietalem  34322  rtelextdg2lem  34469  esumsnf  34807  esummulc1  34824  measxun2  34954  omsmeas  35066  sibfof  35083  probun  35162  signstfvn  35309  bnj517  35626  ecscottd  35885  brlexod  36040  brr0d  36042  ex-sategoelel  36394  mrsubfval  36481  msrval  36511  dfrdg2  36772  itgeq12i  37210  mh-inf3f1  37544  bj-prmoore  38306  bj-bary1lem1  38500  rdgeqoa  38561  finxpreclem2  38581  finxpreclem3  38584  poimirlem1  38807  poimirlem2  38808  poimirlem3  38809  poimirlem4  38810  poimirlem5  38811  poimirlem6  38812  poimirlem7  38813  poimirlem10  38816  poimirlem11  38817  poimirlem12  38818  poimirlem14  38820  poimirlem15  38821  poimirlem17  38823  poimirlem20  38826  poimirlem22  38828  poimirlem23  38829  poimirlem24  38830  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  mblfinlem2  38844  mblfinlem3  38845  ismblfin  38847  mbfposadd  38853  itg2addnclem  38857  itg2addnclem3  38859  itg2addnc  38860  ftc1anclem8  38886  areacirc  38899  ismtyval  39000  ismrer1  39038  grposnOLD  39082  rabeq12f  39355  csbeq12  39356  iuneq12f  39361  lsatcv1  40371  glbconN  40700  atltcvr  40758  3dim2  40791  islln2a  40840  2at0mat0  40848  islpln2a  40871  islvol2aN  40915  pmodlem2  41170  pmapjat1  41176  pcl0bN  41246  osumclN  41290  pexmidALTN  41301  lhp2at0nle  41358  4atexlemunv  41389  cdleme18b  41615  cdleme31sn1  41704  cdleme31sde  41708  cdleme31sn2  41712  ltrniotavalbN  41907  trljco  42063  cdlemh  42140  cdlemk40t  42241  cdlemk40f  42242  cdleml9  42307  dihmeetlem3N  42628  dochkrshp  42709  dihprrn  42749  dihjat1  42752  dvh3dim  42769  dochkrsm  42781  dochexmid  42791  lcfl7lem  42822  lcfl9a  42828  lclkrlem1  42829  mapdspex  42991  mapdindp2  43044  mapdh6dN  43062  hdmap1l6d  43136  hdmap11lem2  43165  hdmap14lem4a  43194  hdmapip0  43238  hlhilset  43257  mulgt0b2d  43808  fiabv  43866  0prjspnrel  43929  jm2.26a  44273  onov0suclim  44537  oe0suclim  44540  cantnfresb  44587  onmcl  44594  omcl2  44596  tfsconcatun  44600  naddwordnexlem4  44664  mnringmulrcld  45487  radcnvrat  45559  sumsnd  46317  icccncfext  47170  fperdvper  47202  dvcosax  47209  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  volioc  47255  itgiccshift  47263  stoweidlem34  47317  dirkercncflem2  47387  fourierdlem32  47422  fourierdlem41  47431  fourierdlem48  47437  fourierdlem64  47453  fourierdlem73  47462  fourierdlem79  47468  fourierdlem82  47471  fourierdlem97  47486  fourierdlem101  47490  fourierdlem109  47498  fourierdlem111  47500  fouriersw  47514  elaa2  47517  etransclem24  47541  etransclem25  47542  etransclem46  47563  nnfoctbdjlem  47738  ismeannd  47750  smfpimltxr  48030  smfpimgtxr  48063  ndfatafv2undef  48555  fzopredsuc  48667  m1modmmod  48707  modlt0b  48712  prproropf1olem3  48860  prproropf1olem4  48861  fmtnorec2lem  48900  2pwp1prmfmtno  48948  sfprmdvdsmersenne  48961  sgprmdvdsmersenne  48962  lighneallem2  48964  lighneallem3  48965  ppivalnnprm  48983  ppivalnnnprmge6  48984  dfodd6  49008  dfeven4  49009  m1expevenALTV  49018  isubgredg  49237  upgrimwlklem5  49272  gricushgr  49288  stgrusgra  49330  isubgr3stgrlem8  49344  clintopval  49574  lmod0rng  49599  zlidlring  49604  2zrngagrp  49619  linplyfv  49711  laznegcl  49736  lazcjcl  49741  dmmpossx2  49780  zlmodzxzscm  49800  zlmodzxzadd  49801  domnmsuppn0  49812  rmsuppss  49813  scmsuppss  49814  ply1mulgsumlem4  49832  ldepsprlem  49915  lincresunit2  49921  nn0sumshdiglemB  50063  2arymptfv  50093  ackval42  50139  affinecomb1  50145  itschlc0yqe  50203  itsclquadb  50219  2itscp  50224  incat  51070  0setrec  51203