Theorem sylan9eqr 2878

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  sbcied2  3815  csbied2  3920  opthhausdorff0  5408  fun2ssres  6399  fcoi1  6552  fcoi2  6553  funssfv  6691  fvtp1  6957  nvof1o  7037  onuninsuci  7555  ot1stg  7703  ot2ndg  7704  el2xptp0  7736  mpomptsx  7762  dmmpossx  7764  fmpox  7765  2ndconst  7796  offsplitfpar  7815  mpoxopoveq  7885  wfrlem10  7964  rdgeq12  8049  rdgsucmptnf  8065  frsucmptn  8074  oev2  8148  oesuclem  8150  oawordeulem  8180  om00  8201  omass  8206  omeulem1  8208  oeoa  8223  oeoe  8225  nnmass  8250  oaabs2  8272  omabs  8274  mapsnend  8588  omxpenlem  8618  sbthlem4  8630  sbthlem6  8632  fodomr  8668  ssenen  8691  fi0  8884  cantnfp1  9144  cnfcomlem  9162  cardaleph  9515  cflim2  9685  axdc4lem  9877  fpwwe2lem12  10063  fpwwe2lem13  10064  rankcf  10199  inatsk  10200  ltrnq  10401  addclprlem1  10438  mulclprlem  10441  1idpr  10451  prlem936  10469  reclem3pr  10471  mulcmpblnrlem  10492  recexsrlem  10525  map2psrpr  10532  addid0  11059  subdivcomb2  11336  nnnn0addcl  11928  zindd  12084  qaddcl  12365  qmulcl  12367  qreccl  12369  xaddnemnf  12630  xaddnepnf  12631  xaddcom  12634  xnegdi  12642  xaddass  12643  xpncan  12645  xleadd1a  12647  xlt2add  12654  rexmul  12665  xmulgt0  12677  xmulge0  12678  xmulasslem3  12680  xlemul1a  12682  xadddilem  12688  xadddi2  12691  modmuladd  13282  modm1p1mod0  13291  modfzo0difsn  13312  seqf1olem2  13411  expp1  13437  expneg  13438  expcllem  13441  mulexp  13469  expmul  13475  sqoddm1div8  13605  bcpasc  13682  hashrabsn01  13735  fseq1hash  13738  hashinfxadd  13747  hashfzo  13791  fnfz0hash  13805  ffzo0hash  13808  hashf1lem1  13814  hashge2el2dif  13839  hashdifsnp1  13855  lsw0  13917  ccatval1  13930  ccatval1OLD  13931  ccatval2  13932  swrdval  14005  ccatopth  14078  reuccatpfxs1  14109  splval  14113  repswswrd  14146  2cshwcshw  14187  s4dom  14281  wrdlen2i  14304  shftfn  14432  reim0b  14478  cjexp  14509  sqeqd  14525  fsumser  15087  sumsnf  15099  binomlem  15184  expcnv  15219  prodsn  15316  prodsnf  15318  bpolylem  15402  bpoly2  15411  bpoly3  15412  ef0lem  15432  dvdsnegb  15627  mod2eq1n2dvds  15696  m1expe  15725  m1expo  15726  m1exp1  15727  flodddiv4  15764  sadadd2lem2  15799  gcdabs  15877  bezoutr1  15913  dvdslcm  15942  lcmeq0  15944  lcmcl  15945  lcmabs  15949  lcmgcdlem  15950  lcmdvds  15952  lcmf0val  15966  lcmftp  15980  lcmfunsnlem2  15984  mulgcddvds  15999  divgcdcoprmex  16010  pcge0  16198  pcadd  16225  pcmpt2  16229  prmreclem4  16255  ramval  16344  ramcl  16365  fvprmselelfz  16380  fvprmselgcd1  16381  ressid2  16552  ressval2  16553  mndind  17992  frmdval  18016  efmnd  18035  smndex1igid  18069  smndex1n0mnd  18077  mgm2nsgrplem3  18085  mulgfval  18226  mulgfvalALT  18227  mulgnn0subcl  18241  mulgnn0z  18254  cycsubm  18345  isga  18421  symgextfve  18547  symgfixf1  18565  f1omvdco2  18576  psgnsn  18648  odid  18666  gexid  18706  efgsval2  18859  frgpuptinv  18897  frgpup2  18902  dprdsn  19158  srgmulgass  19281  srgpcomp  19282  srgbinomlem4  19293  ringinvnzdiv  19343  f1ghm0to0  19492  f1rhm0to0OLD  19493  f1rhm0to0ALT  19494  isabvd  19591  issrng  19621  lmodvsmmulgdi  19669  mptscmfsupp0  19699  lvecinv  19885  lspdisj2  19899  lspfixed  19900  lspexch  19901  sralem  19949  srasca  19953  sravsca  19954  sraip  19955  assamulgscmlem2  20129  mplval  20208  opsrval  20255  cply1mul  20462  gsummoncoe1  20472  evl1fval  20491  znval  20682  psgndiflemB  20744  isphl  20772  scmate  21119  scmatscm  21122  mdetdiagid  21209  mdetunilem7  21227  mdetuni0  21230  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  slesolinvbi  21290  cpmatacl  21324  cpmatinvcl  21325  pmatcollpw2lem  21385  monmatcollpw  21387  pmatcollpwfi  21390  mp2pm2mplem4  21417  pm2mp  21433  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmadumatpoly  21491  cayhamlem4  21496  cayleyhamilton0  21497  cayleyhamiltonALT  21499  indistopon  21609  0ntr  21679  pnrmopn  21951  reftr  22122  kgenval  22143  pt1hmeo  22414  fmval  22551  fmf  22553  istmd  22682  istgp  22685  tsmsval2  22738  isxmet2d  22937  xpsxmetlem  22989  xpsmet  22992  blfvalps  22993  tmsval  23091  isnlm  23284  nmoleub  23340  idnghm  23352  blssioo  23403  blcvx  23406  icccvx  23554  pcorevlem  23630  isclm  23668  caufval  23878  iscms  23948  mbfsup  24265  i1f1  24291  dvexp3  24575  rolle  24587  dvivth  24607  deg1add  24697  0dgr  24835  coefv0  24838  elqaalem2  24909  dvradcnv  25009  abelthlem8  25027  efper  25065  logtayl  25243  abscxpbnd  25334  relogbcxpb  25365  logbgcd1irr  25372  dcubic2  25422  rlimcnp2  25544  cvxcl  25562  zetacvg  25592  lgamgulmlem2  25607  vmaval  25690  chtub  25788  logexprlim  25801  dchrsum2  25844  sumdchr2  25846  bposlem2  25861  lgsdir  25908  lgsne0  25911  lgsdirnn0  25920  lgsdinn0  25921  lgsquadlem2  25957  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2sqn0  26010  dchrvmasum2if  26073  dchrvmasumiflem1  26077  rpvmasum2  26088  pntpbnd1  26162  ostth2lem4  26212  trgcgrg  26301  tgcgr4  26317  ax5seglem1  26714  ax5seglem2  26715  ax5seglem5  26719  usgr1vr  27037  cplgr2vpr  27215  cplgr3v  27217  cusgrrusgr  27363  wlklenvm1  27403  wlk0prc  27435  wlksoneq1eq2  27446  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  crctcshlem4  27598  crctcsh  27602  wlkiswwlks1  27645  wwlksnext  27671  wwlksnextbi  27672  wwlksnextwrd  27675  midwwlks2s3  27731  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2a4  27775  clwlkclwwlklem3  27779  clwwisshclwws  27793  erclwwlkeqlen  27797  clwwlkinwwlk  27818  clwwlkn2  27822  clwwlkf  27826  clwwlkf1  27828  eleclclwwlknlem2  27840  erclwwlkneqlen  27847  umgrhashecclwwlk  27857  eucrctshift  28022  eucrct2eupth  28024  fusgr2wsp2nb  28113  grpoidinvlem2  28282  vcz  28352  nvz  28446  lnon0  28575  ipasslem2  28609  htthlem  28694  hvpncan  28816  hiidge0  28875  normgt0  28904  hsn0elch  29025  shsel3  29092  spansneleq  29347  normcan  29353  h1datomi  29358  fh1  29395  spansncvi  29429  5oalem1  29431  5oalem3  29433  5oalem5  29435  3oalem2  29440  pjdsi  29489  kbpj  29733  0hmop  29760  0lnfn  29762  adj0  29771  nlelshi  29837  branmfn  29882  opsqrlem1  29917  hst1h  30004  mdsl0  30087  superpos  30131  sumdmdlem  30195  cdj3lem1  30211  f1od2  30457  xrpxdivcld  30611  xrge0npcan  30681  resvid2  30901  resvval2  30902  esumsnf  31323  esummulc1  31340  measxun2  31469  omsmeas  31581  sibfof  31598  probun  31677  signstfvn  31839  bnj517  32157  pthhashvtx  32374  ex-sategoelel  32668  mrsubfval  32755  msrval  32785  dfrdg2  33040  bj-prmoore  34410  bj-bary1lem1  34595  rdgeqoa  34654  finxpreclem2  34674  finxpreclem3  34677  matunitlindflem1  34903  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem14  34921  poimirlem15  34922  poimirlem17  34924  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  mblfinlem2  34945  mblfinlem3  34946  ismblfin  34948  mbfposadd  34954  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  ftc1anclem8  34989  areacirc  35002  ismtyval  35093  ismrer1  35131  grposnOLD  35175  rabeq12f  35450  csbeq12  35451  iuneq12f  35456  lsatcv1  36199  glbconN  36528  atltcvr  36586  3dim2  36619  islln2a  36668  2at0mat0  36676  islpln2a  36699  islvol2aN  36743  pmodlem2  36998  pmapjat1  37004  pcl0bN  37074  osumclN  37118  pexmidALTN  37129  lhp2at0nle  37186  4atexlemunv  37217  cdleme18b  37443  cdleme31sn1  37532  cdleme31sde  37536  cdleme31sn2  37540  ltrniotavalbN  37735  trljco  37891  cdlemh  37968  cdlemk40t  38069  cdlemk40f  38070  cdleml9  38135  dihmeetlem3N  38456  dochkrshp  38537  dihprrn  38577  dihjat1  38580  dvh3dim  38597  dochkrsm  38609  dochexmid  38619  lcfl7lem  38650  lcfl9a  38656  lclkrlem1  38657  mapdspex  38819  mapdindp2  38872  mapdh6dN  38890  hdmap1l6d  38964  hdmap11lem2  38993  hdmap14lem4a  39022  hdmapip0  39066  hlhilset  39085  nnadd1com  39209  0prjspnrel  39318  jm2.26a  39646  radcnvrat  40695  sumsnd  41332  icccncfext  42219  fperdvper  42252  dvcosax  42260  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  volioc  42306  itgiccshift  42314  stoweidlem34  42368  dirkercncflem2  42438  fourierdlem32  42473  fourierdlem41  42482  fourierdlem48  42488  fourierdlem64  42504  fourierdlem73  42513  fourierdlem79  42519  fourierdlem82  42522  fourierdlem97  42537  fourierdlem101  42541  fourierdlem109  42549  fourierdlem111  42551  fouriersw  42565  elaa2  42568  etransclem24  42592  etransclem25  42593  etransclem46  42614  nnfoctbdjlem  42786  ismeannd  42798  ndfatafv2undef  43460  fzopredsuc  43572  prproropf1olem3  43716  prproropf1olem4  43717  fmtnorec2lem  43753  2pwp1prmfmtno  43801  sfprmdvdsmersenne  43817  sgprmdvdsmersenne  43818  lighneallem2  43820  lighneallem3  43821  dfodd6  43851  dfeven4  43852  m1expevenALTV  43861  isomushgr  44040  isomuspgrlem2d  44045  clintopval  44160  lmod0rng  44188  zlidlring  44248  2zrngagrp  44263  rngcval  44282  ringcval  44328  dmmpossx2  44434  zlmodzxzscm  44454  zlmodzxzadd  44455  domnmsuppn0  44466  rmsuppss  44467  scmsuppss  44469  ply1mulgsumlem4  44492  ldepsprlem  44576  lincresunit2  44582  m1modmmod  44630  nn0sumshdiglemB  44729  affinecomb1  44738  itschlc0yqe  44796  itsclquadb  44812  2itscp  44817  0setrec  44855