Theorem sylan9eqr 2792

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 2790	. 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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  sbcied2  3810  csbied2  3911  opthhausdorff0  5493  fun2ssres  6580  fcoi1  6751  fcoi2  6752  funssfv  6896  fvtp1  7186  nvof1o  7272  onuninsuci  7833  ot1stg  8000  ot2ndg  8001  el2xptp0  8033  mpomptsx  8061  dmmpossx  8063  fmpox  8064  2ndconst  8098  offsplitfpar  8116  mpoxopoveq  8216  wfrlem10OLD  8330  rdgeq12  8425  rdgsucmptnf  8441  frsucmptn  8451  oev2  8533  oesuclem  8535  oawordeulem  8564  om00  8585  omass  8590  omeulem1  8592  oeoa  8607  oeoe  8609  nnmass  8634  oaabs2  8659  omabs  8661  mapsnend  9048  omxpenlem  9085  sbthlem4  9098  sbthlem6  9100  fodomr  9140  ssenen  9163  fodomfir  9338  fi0  9430  cantnfp1  9693  cnfcomlem  9711  ttrclselem2  9738  cardaleph  10101  cflim2  10275  axdc4lem  10467  fpwwe2lem11  10653  fpwwe2lem12  10654  rankcf  10789  inatsk  10790  ltrnq  10991  addclprlem1  11028  mulclprlem  11031  1idpr  11041  prlem936  11059  reclem3pr  11061  mulcmpblnrlem  11082  recexsrlem  11115  map2psrpr  11122  addid0  11654  subdivcomb2  11935  nnnn0addcl  12529  zindd  12692  qaddcl  12979  qmulcl  12981  qreccl  12983  xaddnemnf  13250  xaddnepnf  13251  xaddcom  13254  xnegdi  13262  xaddass  13263  xpncan  13265  xleadd1a  13267  xlt2add  13274  rexmul  13285  xmulgt0  13297  xmulge0  13298  xmulasslem3  13300  xlemul1a  13302  xadddilem  13308  xadddi2  13311  modmuladd  13929  modm1p1mod0  13938  modfzo0difsn  13959  seqf1olem2  14058  expp1  14084  expneg  14085  expcllem  14088  mulexp  14117  expmul  14123  sqoddm1div8  14259  bcpasc  14337  hashrabsn01  14389  fseq1hash  14392  hashinfxadd  14401  hashfzo  14445  fnfz0hash  14462  ffzo0hash  14465  hashf1lem1  14471  hashge2el2dif  14496  hash3tpexb  14510  hashdifsnp1  14522  lsw0  14581  ccatval1  14593  ccatval2  14594  swrdval  14659  ccatopth  14732  reuccatpfxs1  14763  splval  14767  repswswrd  14800  2cshwcshw  14842  s4dom  14936  wrdlen2i  14959  shftfn  15090  reim0b  15136  cjexp  15167  sqeqd  15183  fsumser  15744  sumsnf  15757  binomlem  15843  expcnv  15878  prodsn  15976  prodsnf  15978  bpolylem  16062  bpoly2  16071  bpoly3  16072  ef0lem  16092  dvdsnegb  16291  mod2eq1n2dvds  16364  m1expe  16391  m1expo  16392  m1exp1  16393  flodddiv4  16432  sadadd2lem2  16467  bezoutr1  16586  dvdslcm  16615  lcmeq0  16617  lcmcl  16618  lcmabs  16622  lcmgcdlem  16623  lcmdvds  16625  lcmf0val  16639  lcmftp  16653  lcmfunsnlem2  16657  mulgcddvds  16672  divgcdcoprmex  16683  pcge0  16880  pcadd  16907  pcmpt2  16911  prmreclem4  16937  ramval  17026  ramcl  17047  fvprmselelfz  17062  fvprmselgcd1  17063  ressid2  17253  ressval2  17254  mndind  18804  frmdval  18827  efmnd  18846  smndex1igid  18880  smndex1n0mnd  18888  mgm2nsgrplem3  18896  mulgfval  19050  mulgfvalALT  19051  mulgnn0subcl  19068  mulgnn0z  19082  cycsubm  19183  f1ghm0to0  19226  isga  19272  symgextfve  19398  symgfixf1  19416  f1omvdco2  19427  psgnsn  19499  odid  19517  gexid  19560  efgsval2  19712  frgpuptinv  19750  frgpup2  19755  dprdsn  20017  srgmulgass  20175  srgpcomp  20176  srgbinomlem4  20187  ringinvnzdiv  20259  rngcval  20576  ringcval  20605  isabvd  20770  issrng  20802  lmodvsmmulgdi  20852  mptscmfsupp0  20882  lvecinv  21072  lspdisj2  21086  lspfixed  21087  lspexch  21088  sralem  21132  srasca  21136  sravsca  21137  sraip  21138  znval  21494  psgndiflemB  21558  isphl  21586  assamulgscmlem2  21858  mplval  21947  opsrval  22002  psdmvr  22105  cply1mul  22232  gsummoncoe1  22244  evl1fval  22264  scmate  22446  scmatscm  22449  mdetdiagid  22536  mdetunilem7  22554  mdetuni0  22557  gsummatr01lem3  22593  gsummatr01lem4  22594  gsummatr01  22595  slesolinvbi  22617  cpmatacl  22652  cpmatinvcl  22653  pmatcollpw2lem  22713  monmatcollpw  22715  pmatcollpwfi  22718  mp2pm2mplem4  22745  pm2mp  22761  cpmadugsumlemF  22812  cpmadugsumfi  22813  cpmadumatpoly  22819  cayhamlem4  22824  cayleyhamilton0  22825  cayleyhamiltonALT  22827  indistopon  22937  0ntr  23007  pnrmopn  23279  reftr  23450  kgenval  23471  pt1hmeo  23742  fmval  23879  fmf  23881  istmd  24010  istgp  24013  tsmsval2  24066  isxmet2d  24264  xpsxmetlem  24316  xpsmet  24319  blfvalps  24320  tmsval  24418  isnlm  24612  nmoleub  24668  idnghm  24680  blssioo  24732  blcvx  24735  icccvx  24897  pcorevlem  24975  isclm  25013  caufval  25225  iscms  25295  mbfsup  25615  i1f1  25641  dvexp3  25932  rolle  25944  dvivth  25965  deg1add  26058  0dgr  26200  coefv0  26203  elqaalem2  26278  dvradcnv  26380  abelthlem8  26399  efper  26438  logtayl  26619  abscxpbnd  26713  relogbcxpb  26747  logbgcd1irr  26754  dcubic2  26804  rlimcnp2  26926  cvxcl  26945  zetacvg  26975  lgamgulmlem2  26990  vmaval  27073  chtub  27173  logexprlim  27186  dchrsum2  27229  sumdchr2  27231  bposlem2  27246  lgsdir  27293  lgsne0  27296  lgsdirnn0  27305  lgsdinn0  27306  lgsquadlem2  27342  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2lgslem3a1  27361  2lgslem3b1  27362  2lgslem3c1  27363  2lgslem3d1  27364  2sqn0  27395  dchrvmasum2if  27458  dchrvmasumiflem1  27462  rpvmasum2  27473  pntpbnd1  27547  ostth2lem4  27597  expsp1  28329  trgcgrg  28440  tgcgr4  28456  ax5seglem1  28853  ax5seglem2  28854  ax5seglem5  28858  usgr1vr  29180  cplgr2vpr  29358  cplgr3v  29360  cusgrrusgr  29507  wlklenvm1  29548  wlk0prc  29580  wlksoneq1eq2  29590  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  crctcshwlkn0lem6  29743  crctcshlem4  29748  crctcsh  29752  wlkiswwlks1  29795  wwlksnext  29821  wwlksnextbi  29822  wwlksnextwrd  29825  midwwlks2s3  29880  clwlkclwwlklem2fv1  29922  clwlkclwwlklem2a4  29924  clwlkclwwlklem3  29928  clwwisshclwws  29942  erclwwlkeqlen  29946  clwwlkinwwlk  29967  clwwlkn2  29971  clwwlkf  29974  clwwlkf1  29976  eleclclwwlknlem2  29988  erclwwlkneqlen  29995  umgrhashecclwwlk  30005  eucrctshift  30170  eucrct2eupth  30172  fusgr2wsp2nb  30261  grpoidinvlem2  30432  vcz  30502  nvz  30596  lnon0  30725  ipasslem2  30759  htthlem  30844  hvpncan  30966  hiidge0  31025  normgt0  31054  hsn0elch  31175  shsel3  31242  spansneleq  31497  normcan  31503  h1datomi  31508  fh1  31545  spansncvi  31579  5oalem1  31581  5oalem3  31583  5oalem5  31585  3oalem2  31590  pjdsi  31639  kbpj  31883  0hmop  31910  0lnfn  31912  adj0  31921  nlelshi  31987  branmfn  32032  opsqrlem1  32067  hst1h  32154  mdsl0  32237  superpos  32281  sumdmdlem  32345  cdj3lem1  32361  f1od2  32644  xrpxdivcld  32855  xrge0npcan  32961  elrgspnlem2  33184  rlocf1  33214  resvid2  33292  resvval2  33293  qsdrng  33458  r1pquslmic  33566  rtelextdg2lem  33706  esumsnf  34041  esummulc1  34058  measxun2  34187  omsmeas  34301  sibfof  34318  probun  34397  signstfvn  34547  bnj517  34862  pthhashvtx  35096  ex-sategoelel  35389  mrsubfval  35476  msrval  35506  dfrdg2  35759  itgeq12i  36170  bj-prmoore  37079  bj-bary1lem1  37275  rdgeqoa  37334  finxpreclem2  37354  finxpreclem3  37357  matunitlindflem1  37586  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem14  37604  poimirlem15  37605  poimirlem17  37607  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  mblfinlem2  37628  mblfinlem3  37629  ismblfin  37631  mbfposadd  37637  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  ftc1anclem8  37670  areacirc  37683  ismtyval  37770  ismrer1  37808  grposnOLD  37852  rabeq12f  38127  csbeq12  38128  iuneq12f  38133  lsatcv1  39012  glbconN  39341  glbconNOLD  39342  atltcvr  39400  3dim2  39433  islln2a  39482  2at0mat0  39490  islpln2a  39513  islvol2aN  39557  pmodlem2  39812  pmapjat1  39818  pcl0bN  39888  osumclN  39932  pexmidALTN  39943  lhp2at0nle  40000  4atexlemunv  40031  cdleme18b  40257  cdleme31sn1  40346  cdleme31sde  40350  cdleme31sn2  40354  ltrniotavalbN  40549  trljco  40705  cdlemh  40782  cdlemk40t  40883  cdlemk40f  40884  cdleml9  40949  dihmeetlem3N  41270  dochkrshp  41351  dihprrn  41391  dihjat1  41394  dvh3dim  41411  dochkrsm  41423  dochexmid  41433  lcfl7lem  41464  lcfl9a  41470  lclkrlem1  41471  mapdspex  41633  mapdindp2  41686  mapdh6dN  41704  hdmap1l6d  41778  hdmap11lem2  41807  hdmap14lem4a  41836  hdmapip0  41880  hlhilset  41899  nnadd1com  42264  fiabv  42506  prjspner1  42596  0prjspnrel  42597  jm2.26a  42971  onov0suclim  43245  oe0suclim  43248  cantnfresb  43295  onmcl  43302  omcl2  43304  tfsconcatun  43308  naddwordnexlem4  43372  mnringmulrcld  44200  radcnvrat  44286  sumsnd  44998  icccncfext  45864  fperdvper  45896  dvcosax  45903  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  volioc  45949  itgiccshift  45957  stoweidlem34  46011  dirkercncflem2  46081  fourierdlem32  46116  fourierdlem41  46125  fourierdlem48  46131  fourierdlem64  46147  fourierdlem73  46156  fourierdlem79  46162  fourierdlem82  46165  fourierdlem97  46180  fourierdlem101  46184  fourierdlem109  46192  fourierdlem111  46194  fouriersw  46208  elaa2  46211  etransclem24  46235  etransclem25  46236  etransclem46  46257  nnfoctbdjlem  46432  ismeannd  46444  smfpimltxr  46724  smfpimgtxr  46757  ndfatafv2undef  47189  fzopredsuc  47300  prproropf1olem3  47467  prproropf1olem4  47468  fmtnorec2lem  47504  2pwp1prmfmtno  47552  sfprmdvdsmersenne  47565  sgprmdvdsmersenne  47566  lighneallem2  47568  lighneallem3  47569  dfodd6  47599  dfeven4  47600  m1expevenALTV  47609  isubgredg  47827  upgrimwlklem5  47862  gricushgr  47878  stgrusgra  47919  isubgr3stgrlem8  47933  clintopval  48127  lmod0rng  48152  zlidlring  48157  2zrngagrp  48172  dmmpossx2  48260  zlmodzxzscm  48280  zlmodzxzadd  48281  domnmsuppn0  48292  rmsuppss  48293  scmsuppss  48294  ply1mulgsumlem4  48313  ldepsprlem  48396  lincresunit2  48402  m1modmmod  48449  nn0sumshdiglemB  48548  2arymptfv  48578  ackval42  48624  affinecomb1  48630  itschlc0yqe  48688  itsclquadb  48704  2itscp  48709  incat  49426  0setrec  49516