Theorem sylan9eqr 2787

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  sbcied2  3801  csbied2  3902  opthhausdorff0  5481  fun2ssres  6564  fcoi1  6737  fcoi2  6738  funssfv  6882  fvtp1  7172  nvof1o  7258  onuninsuci  7819  ot1stg  7985  ot2ndg  7986  el2xptp0  8018  mpomptsx  8046  dmmpossx  8048  fmpox  8049  2ndconst  8083  offsplitfpar  8101  mpoxopoveq  8201  rdgeq12  8384  rdgsucmptnf  8400  frsucmptn  8410  oev2  8490  oesuclem  8492  oawordeulem  8521  om00  8542  omass  8547  omeulem1  8549  oeoa  8564  oeoe  8566  nnmass  8591  oaabs2  8616  omabs  8618  mapsnend  9010  omxpenlem  9047  sbthlem4  9060  sbthlem6  9062  fodomr  9098  ssenen  9121  fodomfir  9286  fi0  9378  cantnfp1  9641  cnfcomlem  9659  ttrclselem2  9686  cardaleph  10049  cflim2  10223  axdc4lem  10415  fpwwe2lem11  10601  fpwwe2lem12  10602  rankcf  10737  inatsk  10738  ltrnq  10939  addclprlem1  10976  mulclprlem  10979  1idpr  10989  prlem936  11007  reclem3pr  11009  mulcmpblnrlem  11030  recexsrlem  11063  map2psrpr  11070  addid0  11604  subdivcomb2  11885  nnnn0addcl  12479  zindd  12642  qaddcl  12931  qmulcl  12933  qreccl  12935  xaddnemnf  13203  xaddnepnf  13204  xaddcom  13207  xnegdi  13215  xaddass  13216  xpncan  13218  xleadd1a  13220  xlt2add  13227  rexmul  13238  xmulgt0  13250  xmulge0  13251  xmulasslem3  13253  xlemul1a  13255  xadddilem  13261  xadddi2  13264  modmuladd  13885  modm1p1mod0  13894  modfzo0difsn  13915  seqf1olem2  14014  expp1  14040  expneg  14041  expcllem  14044  mulexp  14073  expmul  14079  sqoddm1div8  14215  bcpasc  14293  hashrabsn01  14345  fseq1hash  14348  hashinfxadd  14357  hashfzo  14401  fnfz0hash  14418  ffzo0hash  14421  hashf1lem1  14427  hashge2el2dif  14452  hash3tpexb  14466  hashdifsnp1  14478  lsw0  14537  ccatval1  14549  ccatval2  14550  swrdval  14615  ccatopth  14688  reuccatpfxs1  14719  splval  14723  repswswrd  14756  2cshwcshw  14798  s4dom  14892  wrdlen2i  14915  shftfn  15046  reim0b  15092  cjexp  15123  sqeqd  15139  fsumser  15703  sumsnf  15716  binomlem  15802  expcnv  15837  prodsn  15935  prodsnf  15937  bpolylem  16021  bpoly2  16030  bpoly3  16031  ef0lem  16051  dvdsnegb  16250  mod2eq1n2dvds  16324  m1expe  16351  m1expo  16352  m1exp1  16353  flodddiv4  16392  sadadd2lem2  16427  bezoutr1  16546  dvdslcm  16575  lcmeq0  16577  lcmcl  16578  lcmabs  16582  lcmgcdlem  16583  lcmdvds  16585  lcmf0val  16599  lcmftp  16613  lcmfunsnlem2  16617  mulgcddvds  16632  divgcdcoprmex  16643  pcge0  16840  pcadd  16867  pcmpt2  16871  prmreclem4  16897  ramval  16986  ramcl  17007  fvprmselelfz  17022  fvprmselgcd1  17023  ressid2  17211  ressval2  17212  mndind  18762  frmdval  18785  efmnd  18804  smndex1igid  18838  smndex1n0mnd  18846  mgm2nsgrplem3  18854  mulgfval  19008  mulgfvalALT  19009  mulgnn0subcl  19026  mulgnn0z  19040  cycsubm  19141  f1ghm0to0  19184  isga  19230  symgextfve  19356  symgfixf1  19374  f1omvdco2  19385  psgnsn  19457  odid  19475  gexid  19518  efgsval2  19670  frgpuptinv  19708  frgpup2  19713  dprdsn  19975  srgmulgass  20133  srgpcomp  20134  srgbinomlem4  20145  ringinvnzdiv  20217  rngcval  20534  ringcval  20563  isabvd  20728  issrng  20760  lmodvsmmulgdi  20810  mptscmfsupp0  20840  lvecinv  21030  lspdisj2  21044  lspfixed  21045  lspexch  21046  sralem  21090  srasca  21094  sravsca  21095  sraip  21096  znval  21452  psgndiflemB  21516  isphl  21544  assamulgscmlem2  21816  mplval  21905  opsrval  21960  psdmvr  22063  cply1mul  22190  gsummoncoe1  22202  evl1fval  22222  scmate  22404  scmatscm  22407  mdetdiagid  22494  mdetunilem7  22512  mdetuni0  22515  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  slesolinvbi  22575  cpmatacl  22610  cpmatinvcl  22611  pmatcollpw2lem  22671  monmatcollpw  22673  pmatcollpwfi  22676  mp2pm2mplem4  22703  pm2mp  22719  cpmadugsumlemF  22770  cpmadugsumfi  22771  cpmadumatpoly  22777  cayhamlem4  22782  cayleyhamilton0  22783  cayleyhamiltonALT  22785  indistopon  22895  0ntr  22965  pnrmopn  23237  reftr  23408  kgenval  23429  pt1hmeo  23700  fmval  23837  fmf  23839  istmd  23968  istgp  23971  tsmsval2  24024  isxmet2d  24222  xpsxmetlem  24274  xpsmet  24277  blfvalps  24278  tmsval  24376  isnlm  24570  nmoleub  24626  idnghm  24638  blssioo  24690  blcvx  24693  icccvx  24855  pcorevlem  24933  isclm  24971  caufval  25182  iscms  25252  mbfsup  25572  i1f1  25598  dvexp3  25889  rolle  25901  dvivth  25922  deg1add  26015  0dgr  26157  coefv0  26160  elqaalem2  26235  dvradcnv  26337  abelthlem8  26356  efper  26395  logtayl  26576  abscxpbnd  26670  relogbcxpb  26704  logbgcd1irr  26711  dcubic2  26761  rlimcnp2  26883  cvxcl  26902  zetacvg  26932  lgamgulmlem2  26947  vmaval  27030  chtub  27130  logexprlim  27143  dchrsum2  27186  sumdchr2  27188  bposlem2  27203  lgsdir  27250  lgsne0  27253  lgsdirnn0  27262  lgsdinn0  27263  lgsquadlem2  27299  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgslem3a1  27318  2lgslem3b1  27319  2lgslem3c1  27320  2lgslem3d1  27321  2sqn0  27352  dchrvmasum2if  27415  dchrvmasumiflem1  27419  rpvmasum2  27430  pntpbnd1  27504  ostth2lem4  27554  expsp1  28322  trgcgrg  28449  tgcgr4  28465  ax5seglem1  28862  ax5seglem2  28863  ax5seglem5  28867  usgr1vr  29189  cplgr2vpr  29367  cplgr3v  29369  cusgrrusgr  29516  wlklenvm1  29557  wlk0prc  29589  wlksoneq1eq2  29599  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem6  29752  crctcshlem4  29757  crctcsh  29761  wlkiswwlks1  29804  wwlksnext  29830  wwlksnextbi  29831  wwlksnextwrd  29834  midwwlks2s3  29889  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2a4  29933  clwlkclwwlklem3  29937  clwwisshclwws  29951  erclwwlkeqlen  29955  clwwlkinwwlk  29976  clwwlkn2  29980  clwwlkf  29983  clwwlkf1  29985  eleclclwwlknlem2  29997  erclwwlkneqlen  30004  umgrhashecclwwlk  30014  eucrctshift  30179  eucrct2eupth  30181  fusgr2wsp2nb  30270  grpoidinvlem2  30441  vcz  30511  nvz  30605  lnon0  30734  ipasslem2  30768  htthlem  30853  hvpncan  30975  hiidge0  31034  normgt0  31063  hsn0elch  31184  shsel3  31251  spansneleq  31506  normcan  31512  h1datomi  31517  fh1  31554  spansncvi  31588  5oalem1  31590  5oalem3  31592  5oalem5  31594  3oalem2  31599  pjdsi  31648  kbpj  31892  0hmop  31919  0lnfn  31921  adj0  31930  nlelshi  31996  branmfn  32041  opsqrlem1  32076  hst1h  32163  mdsl0  32246  superpos  32290  sumdmdlem  32354  cdj3lem1  32370  f1od2  32651  xrpxdivcld  32862  xrge0npcan  32968  elrgspnlem2  33201  rlocf1  33231  resvid2  33309  resvval2  33310  qsdrng  33475  r1pquslmic  33583  rtelextdg2lem  33723  esumsnf  34061  esummulc1  34078  measxun2  34207  omsmeas  34321  sibfof  34338  probun  34417  signstfvn  34567  bnj517  34882  pthhashvtx  35122  ex-sategoelel  35415  mrsubfval  35502  msrval  35532  dfrdg2  35790  itgeq12i  36201  bj-prmoore  37110  bj-bary1lem1  37306  rdgeqoa  37365  finxpreclem2  37385  finxpreclem3  37388  matunitlindflem1  37617  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem14  37635  poimirlem15  37636  poimirlem17  37638  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  mblfinlem2  37659  mblfinlem3  37660  ismblfin  37662  mbfposadd  37668  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  ftc1anclem8  37701  areacirc  37714  ismtyval  37801  ismrer1  37839  grposnOLD  37883  rabeq12f  38158  csbeq12  38159  iuneq12f  38164  lsatcv1  39048  glbconN  39377  glbconNOLD  39378  atltcvr  39436  3dim2  39469  islln2a  39518  2at0mat0  39526  islpln2a  39549  islvol2aN  39593  pmodlem2  39848  pmapjat1  39854  pcl0bN  39924  osumclN  39968  pexmidALTN  39979  lhp2at0nle  40036  4atexlemunv  40067  cdleme18b  40293  cdleme31sn1  40382  cdleme31sde  40386  cdleme31sn2  40390  ltrniotavalbN  40585  trljco  40741  cdlemh  40818  cdlemk40t  40919  cdlemk40f  40920  cdleml9  40985  dihmeetlem3N  41306  dochkrshp  41387  dihprrn  41427  dihjat1  41430  dvh3dim  41447  dochkrsm  41459  dochexmid  41469  lcfl7lem  41500  lcfl9a  41506  lclkrlem1  41507  mapdspex  41669  mapdindp2  41722  mapdh6dN  41740  hdmap1l6d  41814  hdmap11lem2  41843  hdmap14lem4a  41872  hdmapip0  41916  hlhilset  41935  nnadd1com  42262  mulgt0b2d  42473  fiabv  42531  prjspner1  42621  0prjspnrel  42622  jm2.26a  42996  onov0suclim  43270  oe0suclim  43273  cantnfresb  43320  onmcl  43327  omcl2  43329  tfsconcatun  43333  naddwordnexlem4  43397  mnringmulrcld  44224  radcnvrat  44310  sumsnd  45027  icccncfext  45892  fperdvper  45924  dvcosax  45931  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  volioc  45977  itgiccshift  45985  stoweidlem34  46039  dirkercncflem2  46109  fourierdlem32  46144  fourierdlem41  46153  fourierdlem48  46159  fourierdlem64  46175  fourierdlem73  46184  fourierdlem79  46190  fourierdlem82  46193  fourierdlem97  46208  fourierdlem101  46212  fourierdlem109  46220  fourierdlem111  46222  fouriersw  46236  elaa2  46239  etransclem24  46263  etransclem25  46264  etransclem46  46285  nnfoctbdjlem  46460  ismeannd  46472  smfpimltxr  46752  smfpimgtxr  46785  ndfatafv2undef  47217  fzopredsuc  47328  m1modmmod  47363  modlt0b  47368  prproropf1olem3  47510  prproropf1olem4  47511  fmtnorec2lem  47547  2pwp1prmfmtno  47595  sfprmdvdsmersenne  47608  sgprmdvdsmersenne  47609  lighneallem2  47611  lighneallem3  47612  dfodd6  47642  dfeven4  47643  m1expevenALTV  47652  isubgredg  47870  upgrimwlklem5  47905  gricushgr  47921  stgrusgra  47962  isubgr3stgrlem8  47976  clintopval  48196  lmod0rng  48221  zlidlring  48226  2zrngagrp  48241  dmmpossx2  48329  zlmodzxzscm  48349  zlmodzxzadd  48350  domnmsuppn0  48361  rmsuppss  48362  scmsuppss  48363  ply1mulgsumlem4  48382  ldepsprlem  48465  lincresunit2  48471  nn0sumshdiglemB  48613  2arymptfv  48643  ackval42  48689  affinecomb1  48695  itschlc0yqe  48753  itsclquadb  48769  2itscp  48774  incat  49594  0setrec  49697