Theorem sylan9eqr 2802

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  sbcied2  3852  csbied2  3961  opthhausdorff0  5537  fun2ssres  6623  fcoi1  6795  fcoi2  6796  funssfv  6941  fvtp1  7232  nvof1o  7316  onuninsuci  7877  ot1stg  8044  ot2ndg  8045  el2xptp0  8077  mpomptsx  8105  dmmpossx  8107  fmpox  8108  2ndconst  8142  offsplitfpar  8160  mpoxopoveq  8260  wfrlem10OLD  8374  rdgeq12  8469  rdgsucmptnf  8485  frsucmptn  8495  oev2  8579  oesuclem  8581  oawordeulem  8610  om00  8631  omass  8636  omeulem1  8638  oeoa  8653  oeoe  8655  nnmass  8680  oaabs2  8705  omabs  8707  mapsnend  9101  omxpenlem  9139  sbthlem4  9152  sbthlem6  9154  fodomr  9194  ssenen  9217  fodomfir  9396  fi0  9489  cantnfp1  9750  cnfcomlem  9768  ttrclselem2  9795  cardaleph  10158  cflim2  10332  axdc4lem  10524  fpwwe2lem11  10710  fpwwe2lem12  10711  rankcf  10846  inatsk  10847  ltrnq  11048  addclprlem1  11085  mulclprlem  11088  1idpr  11098  prlem936  11116  reclem3pr  11118  mulcmpblnrlem  11139  recexsrlem  11172  map2psrpr  11179  addid0  11709  subdivcomb2  11990  nnnn0addcl  12583  zindd  12744  qaddcl  13030  qmulcl  13032  qreccl  13034  xaddnemnf  13298  xaddnepnf  13299  xaddcom  13302  xnegdi  13310  xaddass  13311  xpncan  13313  xleadd1a  13315  xlt2add  13322  rexmul  13333  xmulgt0  13345  xmulge0  13346  xmulasslem3  13348  xlemul1a  13350  xadddilem  13356  xadddi2  13359  modmuladd  13964  modm1p1mod0  13973  modfzo0difsn  13994  seqf1olem2  14093  expp1  14119  expneg  14120  expcllem  14123  mulexp  14152  expmul  14158  sqoddm1div8  14292  bcpasc  14370  hashrabsn01  14422  fseq1hash  14425  hashinfxadd  14434  hashfzo  14478  fnfz0hash  14495  ffzo0hash  14498  hashf1lem1  14504  hashge2el2dif  14529  hash3tpexb  14543  hashdifsnp1  14555  lsw0  14613  ccatval1  14625  ccatval2  14626  swrdval  14691  ccatopth  14764  reuccatpfxs1  14795  splval  14799  repswswrd  14832  2cshwcshw  14874  s4dom  14968  wrdlen2i  14991  shftfn  15122  reim0b  15168  cjexp  15199  sqeqd  15215  fsumser  15778  sumsnf  15791  binomlem  15877  expcnv  15912  prodsn  16010  prodsnf  16012  bpolylem  16096  bpoly2  16105  bpoly3  16106  ef0lem  16126  dvdsnegb  16322  mod2eq1n2dvds  16395  m1expe  16422  m1expo  16423  m1exp1  16424  flodddiv4  16461  sadadd2lem2  16496  gcdabsOLD  16578  bezoutr1  16616  dvdslcm  16645  lcmeq0  16647  lcmcl  16648  lcmabs  16652  lcmgcdlem  16653  lcmdvds  16655  lcmf0val  16669  lcmftp  16683  lcmfunsnlem2  16687  mulgcddvds  16702  divgcdcoprmex  16713  pcge0  16909  pcadd  16936  pcmpt2  16940  prmreclem4  16966  ramval  17055  ramcl  17076  fvprmselelfz  17091  fvprmselgcd1  17092  ressid2  17291  ressval2  17292  mndind  18863  frmdval  18886  efmnd  18905  smndex1igid  18939  smndex1n0mnd  18947  mgm2nsgrplem3  18955  mulgfval  19109  mulgfvalALT  19110  mulgnn0subcl  19127  mulgnn0z  19141  cycsubm  19242  f1ghm0to0  19285  isga  19331  symgextfve  19461  symgfixf1  19479  f1omvdco2  19490  psgnsn  19562  odid  19580  gexid  19623  efgsval2  19775  frgpuptinv  19813  frgpup2  19818  dprdsn  20080  srgmulgass  20244  srgpcomp  20245  srgbinomlem4  20256  ringinvnzdiv  20324  rngcval  20640  ringcval  20669  isabvd  20835  issrng  20867  lmodvsmmulgdi  20917  mptscmfsupp0  20947  lvecinv  21138  lspdisj2  21152  lspfixed  21153  lspexch  21154  sralem  21198  sralemOLD  21199  srasca  21206  srascaOLD  21207  sravsca  21208  sravscaOLD  21209  sraip  21210  znval  21573  psgndiflemB  21641  isphl  21669  assamulgscmlem2  21943  mplval  22032  opsrval  22087  cply1mul  22321  gsummoncoe1  22333  evl1fval  22353  scmate  22537  scmatscm  22540  mdetdiagid  22627  mdetunilem7  22645  mdetuni0  22648  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  slesolinvbi  22708  cpmatacl  22743  cpmatinvcl  22744  pmatcollpw2lem  22804  monmatcollpw  22806  pmatcollpwfi  22809  mp2pm2mplem4  22836  pm2mp  22852  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmadumatpoly  22910  cayhamlem4  22915  cayleyhamilton0  22916  cayleyhamiltonALT  22918  indistopon  23029  0ntr  23100  pnrmopn  23372  reftr  23543  kgenval  23564  pt1hmeo  23835  fmval  23972  fmf  23974  istmd  24103  istgp  24106  tsmsval2  24159  isxmet2d  24358  xpsxmetlem  24410  xpsmet  24413  blfvalps  24414  tmsval  24514  isnlm  24717  nmoleub  24773  idnghm  24785  blssioo  24836  blcvx  24839  icccvx  25000  pcorevlem  25078  isclm  25116  caufval  25328  iscms  25398  mbfsup  25718  i1f1  25744  dvexp3  26036  rolle  26048  dvivth  26069  deg1add  26162  0dgr  26304  coefv0  26307  elqaalem2  26380  dvradcnv  26482  abelthlem8  26501  efper  26539  logtayl  26720  abscxpbnd  26814  relogbcxpb  26848  logbgcd1irr  26855  dcubic2  26905  rlimcnp2  27027  cvxcl  27046  zetacvg  27076  lgamgulmlem2  27091  vmaval  27174  chtub  27274  logexprlim  27287  dchrsum2  27330  sumdchr2  27332  bposlem2  27347  lgsdir  27394  lgsne0  27397  lgsdirnn0  27406  lgsdinn0  27407  lgsquadlem2  27443  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgslem3d1  27465  2sqn0  27496  dchrvmasum2if  27559  dchrvmasumiflem1  27563  rpvmasum2  27574  pntpbnd1  27648  ostth2lem4  27698  expsp1  28430  trgcgrg  28541  tgcgr4  28557  ax5seglem1  28961  ax5seglem2  28962  ax5seglem5  28966  usgr1vr  29290  cplgr2vpr  29468  cplgr3v  29470  cusgrrusgr  29617  wlklenvm1  29658  wlk0prc  29690  wlksoneq1eq2  29700  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  crctcshlem4  29853  crctcsh  29857  wlkiswwlks1  29900  wwlksnext  29926  wwlksnextbi  29927  wwlksnextwrd  29930  midwwlks2s3  29985  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2a4  30029  clwlkclwwlklem3  30033  clwwisshclwws  30047  erclwwlkeqlen  30051  clwwlkinwwlk  30072  clwwlkn2  30076  clwwlkf  30079  clwwlkf1  30081  eleclclwwlknlem2  30093  erclwwlkneqlen  30100  umgrhashecclwwlk  30110  eucrctshift  30275  eucrct2eupth  30277  fusgr2wsp2nb  30366  grpoidinvlem2  30537  vcz  30607  nvz  30701  lnon0  30830  ipasslem2  30864  htthlem  30949  hvpncan  31071  hiidge0  31130  normgt0  31159  hsn0elch  31280  shsel3  31347  spansneleq  31602  normcan  31608  h1datomi  31613  fh1  31650  spansncvi  31684  5oalem1  31686  5oalem3  31688  5oalem5  31690  3oalem2  31695  pjdsi  31744  kbpj  31988  0hmop  32015  0lnfn  32017  adj0  32026  nlelshi  32092  branmfn  32137  opsqrlem1  32172  hst1h  32259  mdsl0  32342  superpos  32386  sumdmdlem  32450  cdj3lem1  32466  f1od2  32735  xrpxdivcld  32899  xrge0npcan  33006  rlocf1  33245  resvid2  33319  resvval2  33320  qsdrng  33490  r1pquslmic  33596  rtelextdg2lem  33717  esumsnf  34028  esummulc1  34045  measxun2  34174  omsmeas  34288  sibfof  34305  probun  34384  signstfvn  34546  bnj517  34861  pthhashvtx  35095  ex-sategoelel  35389  mrsubfval  35476  msrval  35506  dfrdg2  35759  itgeq12i  36170  bj-prmoore  37081  bj-bary1lem1  37277  rdgeqoa  37336  finxpreclem2  37356  finxpreclem3  37359  matunitlindflem1  37576  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem14  37594  poimirlem15  37595  poimirlem17  37597  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  mblfinlem2  37618  mblfinlem3  37619  ismblfin  37621  mbfposadd  37627  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  ftc1anclem8  37660  areacirc  37673  ismtyval  37760  ismrer1  37798  grposnOLD  37842  rabeq12f  38117  csbeq12  38118  iuneq12f  38123  lsatcv1  39004  glbconN  39333  glbconNOLD  39334  atltcvr  39392  3dim2  39425  islln2a  39474  2at0mat0  39482  islpln2a  39505  islvol2aN  39549  pmodlem2  39804  pmapjat1  39810  pcl0bN  39880  osumclN  39924  pexmidALTN  39935  lhp2at0nle  39992  4atexlemunv  40023  cdleme18b  40249  cdleme31sn1  40338  cdleme31sde  40342  cdleme31sn2  40346  ltrniotavalbN  40541  trljco  40697  cdlemh  40774  cdlemk40t  40875  cdlemk40f  40876  cdleml9  40941  dihmeetlem3N  41262  dochkrshp  41343  dihprrn  41383  dihjat1  41386  dvh3dim  41403  dochkrsm  41415  dochexmid  41425  lcfl7lem  41456  lcfl9a  41462  lclkrlem1  41463  mapdspex  41625  mapdindp2  41678  mapdh6dN  41696  hdmap1l6d  41770  hdmap11lem2  41799  hdmap14lem4a  41828  hdmapip0  41872  hlhilset  41891  nnadd1com  42256  fiabv  42491  prjspner1  42581  0prjspnrel  42582  jm2.26a  42957  onov0suclim  43236  oe0suclim  43239  cantnfresb  43286  onmcl  43293  omcl2  43295  tfsconcatun  43299  naddwordnexlem4  43363  mnringmulrcld  44197  radcnvrat  44283  sumsnd  44926  icccncfext  45808  fperdvper  45840  dvcosax  45847  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  volioc  45893  itgiccshift  45901  stoweidlem34  45955  dirkercncflem2  46025  fourierdlem32  46060  fourierdlem41  46069  fourierdlem48  46075  fourierdlem64  46091  fourierdlem73  46100  fourierdlem79  46106  fourierdlem82  46109  fourierdlem97  46124  fourierdlem101  46128  fourierdlem109  46136  fourierdlem111  46138  fouriersw  46152  elaa2  46155  etransclem24  46179  etransclem25  46180  etransclem46  46201  nnfoctbdjlem  46376  ismeannd  46388  smfpimltxr  46668  smfpimgtxr  46701  ndfatafv2undef  47127  fzopredsuc  47238  prproropf1olem3  47379  prproropf1olem4  47380  fmtnorec2lem  47416  2pwp1prmfmtno  47464  sfprmdvdsmersenne  47477  sgprmdvdsmersenne  47478  lighneallem2  47480  lighneallem3  47481  dfodd6  47511  dfeven4  47512  m1expevenALTV  47521  gricushgr  47770  clintopval  47927  lmod0rng  47952  zlidlring  47957  2zrngagrp  47972  dmmpossx2  48061  zlmodzxzscm  48082  zlmodzxzadd  48083  domnmsuppn0  48094  rmsuppss  48095  scmsuppss  48097  ply1mulgsumlem4  48118  ldepsprlem  48201  lincresunit2  48207  m1modmmod  48255  nn0sumshdiglemB  48354  2arymptfv  48384  ackval42  48430  affinecomb1  48436  itschlc0yqe  48494  itsclquadb  48510  2itscp  48515  0setrec  48796