Theorem sylan9eqr 2796

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  sbcied2  3838  csbied2  3947  opthhausdorff0  5527  fun2ssres  6612  fcoi1  6782  fcoi2  6783  funssfv  6927  fvtp1  7214  nvof1o  7299  onuninsuci  7860  ot1stg  8026  ot2ndg  8027  el2xptp0  8059  mpomptsx  8087  dmmpossx  8089  fmpox  8090  2ndconst  8124  offsplitfpar  8142  mpoxopoveq  8242  wfrlem10OLD  8356  rdgeq12  8451  rdgsucmptnf  8467  frsucmptn  8477  oev2  8559  oesuclem  8561  oawordeulem  8590  om00  8611  omass  8616  omeulem1  8618  oeoa  8633  oeoe  8635  nnmass  8660  oaabs2  8685  omabs  8687  mapsnend  9074  omxpenlem  9111  sbthlem4  9124  sbthlem6  9126  fodomr  9166  ssenen  9189  fodomfir  9365  fi0  9457  cantnfp1  9718  cnfcomlem  9736  ttrclselem2  9763  cardaleph  10126  cflim2  10300  axdc4lem  10492  fpwwe2lem11  10678  fpwwe2lem12  10679  rankcf  10814  inatsk  10815  ltrnq  11016  addclprlem1  11053  mulclprlem  11056  1idpr  11066  prlem936  11084  reclem3pr  11086  mulcmpblnrlem  11107  recexsrlem  11140  map2psrpr  11147  addid0  11679  subdivcomb2  11960  nnnn0addcl  12553  zindd  12716  qaddcl  13004  qmulcl  13006  qreccl  13008  xaddnemnf  13274  xaddnepnf  13275  xaddcom  13278  xnegdi  13286  xaddass  13287  xpncan  13289  xleadd1a  13291  xlt2add  13298  rexmul  13309  xmulgt0  13321  xmulge0  13322  xmulasslem3  13324  xlemul1a  13326  xadddilem  13332  xadddi2  13335  modmuladd  13950  modm1p1mod0  13959  modfzo0difsn  13980  seqf1olem2  14079  expp1  14105  expneg  14106  expcllem  14109  mulexp  14138  expmul  14144  sqoddm1div8  14278  bcpasc  14356  hashrabsn01  14408  fseq1hash  14411  hashinfxadd  14420  hashfzo  14464  fnfz0hash  14481  ffzo0hash  14484  hashf1lem1  14490  hashge2el2dif  14515  hash3tpexb  14529  hashdifsnp1  14541  lsw0  14599  ccatval1  14611  ccatval2  14612  swrdval  14677  ccatopth  14750  reuccatpfxs1  14781  splval  14785  repswswrd  14818  2cshwcshw  14860  s4dom  14954  wrdlen2i  14977  shftfn  15108  reim0b  15154  cjexp  15185  sqeqd  15201  fsumser  15762  sumsnf  15775  binomlem  15861  expcnv  15896  prodsn  15994  prodsnf  15996  bpolylem  16080  bpoly2  16089  bpoly3  16090  ef0lem  16110  dvdsnegb  16307  mod2eq1n2dvds  16380  m1expe  16407  m1expo  16408  m1exp1  16409  flodddiv4  16448  sadadd2lem2  16483  bezoutr1  16602  dvdslcm  16631  lcmeq0  16633  lcmcl  16634  lcmabs  16638  lcmgcdlem  16639  lcmdvds  16641  lcmf0val  16655  lcmftp  16669  lcmfunsnlem2  16673  mulgcddvds  16688  divgcdcoprmex  16699  pcge0  16895  pcadd  16922  pcmpt2  16926  prmreclem4  16952  ramval  17041  ramcl  17062  fvprmselelfz  17077  fvprmselgcd1  17078  ressid2  17277  ressval2  17278  mndind  18853  frmdval  18876  efmnd  18895  smndex1igid  18929  smndex1n0mnd  18937  mgm2nsgrplem3  18945  mulgfval  19099  mulgfvalALT  19100  mulgnn0subcl  19117  mulgnn0z  19131  cycsubm  19232  f1ghm0to0  19275  isga  19321  symgextfve  19451  symgfixf1  19469  f1omvdco2  19480  psgnsn  19552  odid  19570  gexid  19613  efgsval2  19765  frgpuptinv  19803  frgpup2  19808  dprdsn  20070  srgmulgass  20234  srgpcomp  20235  srgbinomlem4  20246  ringinvnzdiv  20314  rngcval  20634  ringcval  20663  isabvd  20829  issrng  20861  lmodvsmmulgdi  20911  mptscmfsupp0  20941  lvecinv  21132  lspdisj2  21146  lspfixed  21147  lspexch  21148  sralem  21192  sralemOLD  21193  srasca  21200  srascaOLD  21201  sravsca  21202  sravscaOLD  21203  sraip  21204  znval  21567  psgndiflemB  21635  isphl  21663  assamulgscmlem2  21937  mplval  22026  opsrval  22081  cply1mul  22315  gsummoncoe1  22327  evl1fval  22347  scmate  22531  scmatscm  22534  mdetdiagid  22621  mdetunilem7  22639  mdetuni0  22642  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  slesolinvbi  22702  cpmatacl  22737  cpmatinvcl  22738  pmatcollpw2lem  22798  monmatcollpw  22800  pmatcollpwfi  22803  mp2pm2mplem4  22830  pm2mp  22846  cpmadugsumlemF  22897  cpmadugsumfi  22898  cpmadumatpoly  22904  cayhamlem4  22909  cayleyhamilton0  22910  cayleyhamiltonALT  22912  indistopon  23023  0ntr  23094  pnrmopn  23366  reftr  23537  kgenval  23558  pt1hmeo  23829  fmval  23966  fmf  23968  istmd  24097  istgp  24100  tsmsval2  24153  isxmet2d  24352  xpsxmetlem  24404  xpsmet  24407  blfvalps  24408  tmsval  24508  isnlm  24711  nmoleub  24767  idnghm  24779  blssioo  24830  blcvx  24833  icccvx  24994  pcorevlem  25072  isclm  25110  caufval  25322  iscms  25392  mbfsup  25712  i1f1  25738  dvexp3  26030  rolle  26042  dvivth  26063  deg1add  26156  0dgr  26298  coefv0  26301  elqaalem2  26376  dvradcnv  26478  abelthlem8  26497  efper  26535  logtayl  26716  abscxpbnd  26810  relogbcxpb  26844  logbgcd1irr  26851  dcubic2  26901  rlimcnp2  27023  cvxcl  27042  zetacvg  27072  lgamgulmlem2  27087  vmaval  27170  chtub  27270  logexprlim  27283  dchrsum2  27326  sumdchr2  27328  bposlem2  27343  lgsdir  27390  lgsne0  27393  lgsdirnn0  27402  lgsdinn0  27403  lgsquadlem2  27439  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2lgslem3a1  27458  2lgslem3b1  27459  2lgslem3c1  27460  2lgslem3d1  27461  2sqn0  27492  dchrvmasum2if  27555  dchrvmasumiflem1  27559  rpvmasum2  27570  pntpbnd1  27644  ostth2lem4  27694  expsp1  28426  trgcgrg  28537  tgcgr4  28553  ax5seglem1  28957  ax5seglem2  28958  ax5seglem5  28962  usgr1vr  29286  cplgr2vpr  29464  cplgr3v  29466  cusgrrusgr  29613  wlklenvm1  29654  wlk0prc  29686  wlksoneq1eq2  29696  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  crctcshlem4  29849  crctcsh  29853  wlkiswwlks1  29896  wwlksnext  29922  wwlksnextbi  29923  wwlksnextwrd  29926  midwwlks2s3  29981  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2a4  30025  clwlkclwwlklem3  30029  clwwisshclwws  30043  erclwwlkeqlen  30047  clwwlkinwwlk  30068  clwwlkn2  30072  clwwlkf  30075  clwwlkf1  30077  eleclclwwlknlem2  30089  erclwwlkneqlen  30096  umgrhashecclwwlk  30106  eucrctshift  30271  eucrct2eupth  30273  fusgr2wsp2nb  30362  grpoidinvlem2  30533  vcz  30603  nvz  30697  lnon0  30826  ipasslem2  30860  htthlem  30945  hvpncan  31067  hiidge0  31126  normgt0  31155  hsn0elch  31276  shsel3  31343  spansneleq  31598  normcan  31604  h1datomi  31609  fh1  31646  spansncvi  31680  5oalem1  31682  5oalem3  31684  5oalem5  31686  3oalem2  31691  pjdsi  31740  kbpj  31984  0hmop  32011  0lnfn  32013  adj0  32022  nlelshi  32088  branmfn  32133  opsqrlem1  32168  hst1h  32255  mdsl0  32338  superpos  32382  sumdmdlem  32446  cdj3lem1  32462  f1od2  32738  xrpxdivcld  32901  xrge0npcan  33007  elrgspnlem2  33232  rlocf1  33259  resvid2  33333  resvval2  33334  qsdrng  33504  r1pquslmic  33610  rtelextdg2lem  33731  esumsnf  34044  esummulc1  34061  measxun2  34190  omsmeas  34304  sibfof  34321  probun  34400  signstfvn  34562  bnj517  34877  pthhashvtx  35111  ex-sategoelel  35405  mrsubfval  35492  msrval  35522  dfrdg2  35776  itgeq12i  36187  bj-prmoore  37097  bj-bary1lem1  37293  rdgeqoa  37352  finxpreclem2  37372  finxpreclem3  37375  matunitlindflem1  37602  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem14  37620  poimirlem15  37621  poimirlem17  37623  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  mblfinlem2  37644  mblfinlem3  37645  ismblfin  37647  mbfposadd  37653  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  ftc1anclem8  37686  areacirc  37699  ismtyval  37786  ismrer1  37824  grposnOLD  37868  rabeq12f  38143  csbeq12  38144  iuneq12f  38149  lsatcv1  39029  glbconN  39358  glbconNOLD  39359  atltcvr  39417  3dim2  39450  islln2a  39499  2at0mat0  39507  islpln2a  39530  islvol2aN  39574  pmodlem2  39829  pmapjat1  39835  pcl0bN  39905  osumclN  39949  pexmidALTN  39960  lhp2at0nle  40017  4atexlemunv  40048  cdleme18b  40274  cdleme31sn1  40363  cdleme31sde  40367  cdleme31sn2  40371  ltrniotavalbN  40566  trljco  40722  cdlemh  40799  cdlemk40t  40900  cdlemk40f  40901  cdleml9  40966  dihmeetlem3N  41287  dochkrshp  41368  dihprrn  41408  dihjat1  41411  dvh3dim  41428  dochkrsm  41440  dochexmid  41450  lcfl7lem  41481  lcfl9a  41487  lclkrlem1  41488  mapdspex  41650  mapdindp2  41703  mapdh6dN  41721  hdmap1l6d  41795  hdmap11lem2  41824  hdmap14lem4a  41853  hdmapip0  41897  hlhilset  41916  nnadd1com  42280  fiabv  42522  prjspner1  42612  0prjspnrel  42613  jm2.26a  42988  onov0suclim  43263  oe0suclim  43266  cantnfresb  43313  onmcl  43320  omcl2  43322  tfsconcatun  43326  naddwordnexlem4  43390  mnringmulrcld  44223  radcnvrat  44309  sumsnd  44963  icccncfext  45842  fperdvper  45874  dvcosax  45881  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  volioc  45927  itgiccshift  45935  stoweidlem34  45989  dirkercncflem2  46059  fourierdlem32  46094  fourierdlem41  46103  fourierdlem48  46109  fourierdlem64  46125  fourierdlem73  46134  fourierdlem79  46140  fourierdlem82  46143  fourierdlem97  46158  fourierdlem101  46162  fourierdlem109  46170  fourierdlem111  46172  fouriersw  46186  elaa2  46189  etransclem24  46213  etransclem25  46214  etransclem46  46235  nnfoctbdjlem  46410  ismeannd  46422  smfpimltxr  46702  smfpimgtxr  46735  ndfatafv2undef  47161  fzopredsuc  47272  prproropf1olem3  47429  prproropf1olem4  47430  fmtnorec2lem  47466  2pwp1prmfmtno  47514  sfprmdvdsmersenne  47527  sgprmdvdsmersenne  47528  lighneallem2  47530  lighneallem3  47531  dfodd6  47561  dfeven4  47562  m1expevenALTV  47571  isubgredg  47789  gricushgr  47823  stgrusgra  47861  isubgr3stgrlem8  47875  clintopval  48047  lmod0rng  48072  zlidlring  48077  2zrngagrp  48092  dmmpossx2  48181  zlmodzxzscm  48201  zlmodzxzadd  48202  domnmsuppn0  48213  rmsuppss  48214  scmsuppss  48215  ply1mulgsumlem4  48234  ldepsprlem  48317  lincresunit2  48323  m1modmmod  48370  nn0sumshdiglemB  48469  2arymptfv  48499  ackval42  48545  affinecomb1  48551  itschlc0yqe  48609  itsclquadb  48625  2itscp  48630  0setrec  48934