Theorem sylan9eqr 2794

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  sbcied2  3787  csbied2  3888  opthhausdorff0  5474  fun2ssres  6545  fcoi1  6716  fcoi2  6717  funssfv  6863  fvtp1  7151  nvof1o  7236  onuninsuci  7792  ot1stg  7957  ot2ndg  7958  el2xptp0  7990  mpomptsx  8018  dmmpossx  8020  fmpox  8021  2ndconst  8053  offsplitfpar  8071  mpoxopoveq  8171  rdgeq12  8354  rdgsucmptnf  8370  frsucmptn  8380  oev2  8460  oesuclem  8462  oawordeulem  8491  om00  8512  omass  8517  omeulem1  8519  oeoa  8535  oeoe  8537  nnmass  8562  oaabs2  8587  omabs  8589  mapsnend  8985  omxpenlem  9018  sbthlem4  9030  sbthlem6  9032  fodomr  9068  ssenen  9091  fodomfir  9240  fi0  9335  cantnfp1  9602  cnfcomlem  9620  ttrclselem2  9647  cardaleph  10011  cflim2  10185  axdc4lem  10377  fpwwe2lem11  10564  fpwwe2lem12  10565  rankcf  10700  inatsk  10701  ltrnq  10902  addclprlem1  10939  mulclprlem  10942  1idpr  10952  prlem936  10970  reclem3pr  10972  mulcmpblnrlem  10993  recexsrlem  11026  map2psrpr  11033  addid0  11568  subdivcomb2  11849  nnnn0addcl  12443  zindd  12605  qaddcl  12890  qmulcl  12892  qreccl  12894  xaddnemnf  13163  xaddnepnf  13164  xaddcom  13167  xnegdi  13175  xaddass  13176  xpncan  13178  xleadd1a  13180  xlt2add  13187  rexmul  13198  xmulgt0  13210  xmulge0  13211  xmulasslem3  13213  xlemul1a  13215  xadddilem  13221  xadddi2  13224  modmuladd  13848  modm1p1mod0  13857  modfzo0difsn  13878  seqf1olem2  13977  expp1  14003  expneg  14004  expcllem  14007  mulexp  14036  expmul  14042  sqoddm1div8  14178  bcpasc  14256  hashrabsn01  14308  fseq1hash  14311  hashinfxadd  14320  hashfzo  14364  fnfz0hash  14381  ffzo0hash  14384  hashf1lem1  14390  hashge2el2dif  14415  hash3tpexb  14429  hashdifsnp1  14441  lsw0  14500  ccatval1  14512  ccatval2  14513  swrdval  14579  ccatopth  14651  reuccatpfxs1  14682  splval  14686  repswswrd  14719  2cshwcshw  14760  s4dom  14854  wrdlen2i  14877  shftfn  15008  reim0b  15054  cjexp  15085  sqeqd  15101  fsumser  15665  sumsnf  15678  binomlem  15764  expcnv  15799  prodsn  15897  prodsnf  15899  bpolylem  15983  bpoly2  15992  bpoly3  15993  ef0lem  16013  dvdsnegb  16212  mod2eq1n2dvds  16286  m1expe  16313  m1expo  16314  m1exp1  16315  flodddiv4  16354  sadadd2lem2  16389  bezoutr1  16508  dvdslcm  16537  lcmeq0  16539  lcmcl  16540  lcmabs  16544  lcmgcdlem  16545  lcmdvds  16547  lcmf0val  16561  lcmftp  16575  lcmfunsnlem2  16579  mulgcddvds  16594  divgcdcoprmex  16605  pcge0  16802  pcadd  16829  pcmpt2  16833  prmreclem4  16859  ramval  16948  ramcl  16969  fvprmselelfz  16984  fvprmselgcd1  16985  ressid2  17173  ressval2  17174  mndind  18765  frmdval  18788  efmnd  18807  smndex1igid  18841  smndex1n0mnd  18849  mgm2nsgrplem3  18857  mulgfval  19011  mulgfvalALT  19012  mulgnn0subcl  19029  mulgnn0z  19043  cycsubm  19143  f1ghm0to0  19186  isga  19232  symgextfve  19360  symgfixf1  19378  f1omvdco2  19389  psgnsn  19461  odid  19479  gexid  19522  efgsval2  19674  frgpuptinv  19712  frgpup2  19717  dprdsn  19979  srgmulgass  20164  srgpcomp  20165  srgbinomlem4  20176  ringinvnzdiv  20248  rngcval  20563  ringcval  20592  isabvd  20757  issrng  20789  lmodvsmmulgdi  20860  mptscmfsupp0  20890  lvecinv  21080  lspdisj2  21094  lspfixed  21095  lspexch  21096  sralem  21140  srasca  21144  sravsca  21145  sraip  21146  znval  21502  psgndiflemB  21567  isphl  21595  assamulgscmlem2  21868  mplval  21956  opsrval  22013  psdmvr  22124  cply1mul  22252  gsummoncoe1  22264  evl1fval  22284  scmate  22466  scmatscm  22469  mdetdiagid  22556  mdetunilem7  22574  mdetuni0  22577  gsummatr01lem3  22613  gsummatr01lem4  22614  gsummatr01  22615  slesolinvbi  22637  cpmatacl  22672  cpmatinvcl  22673  pmatcollpw2lem  22733  monmatcollpw  22735  pmatcollpwfi  22738  mp2pm2mplem4  22765  pm2mp  22781  cpmadugsumlemF  22832  cpmadugsumfi  22833  cpmadumatpoly  22839  cayhamlem4  22844  cayleyhamilton0  22845  cayleyhamiltonALT  22847  indistopon  22957  0ntr  23027  pnrmopn  23299  reftr  23470  kgenval  23491  pt1hmeo  23762  fmval  23899  fmf  23901  istmd  24030  istgp  24033  tsmsval2  24086  isxmet2d  24283  xpsxmetlem  24335  xpsmet  24338  blfvalps  24339  tmsval  24437  isnlm  24631  nmoleub  24687  idnghm  24699  blssioo  24751  blcvx  24754  icccvx  24916  pcorevlem  24994  isclm  25032  caufval  25243  iscms  25313  mbfsup  25633  i1f1  25659  dvexp3  25950  rolle  25962  dvivth  25983  deg1add  26076  0dgr  26218  coefv0  26221  elqaalem2  26296  dvradcnv  26398  abelthlem8  26417  efper  26456  logtayl  26637  abscxpbnd  26731  relogbcxpb  26765  logbgcd1irr  26772  dcubic2  26822  rlimcnp2  26944  cvxcl  26963  zetacvg  26993  lgamgulmlem2  27008  vmaval  27091  chtub  27191  logexprlim  27204  dchrsum2  27247  sumdchr2  27249  bposlem2  27264  lgsdir  27311  lgsne0  27314  lgsdirnn0  27323  lgsdinn0  27324  lgsquadlem2  27360  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  2sqn0  27413  dchrvmasum2if  27476  dchrvmasumiflem1  27480  rpvmasum2  27491  pntpbnd1  27565  ostth2lem4  27615  expsp1  28437  trgcgrg  28599  tgcgr4  28615  ax5seglem1  29013  ax5seglem2  29014  ax5seglem5  29018  usgr1vr  29340  cplgr2vpr  29518  cplgr3v  29520  cusgrrusgr  29667  wlklenvm1  29707  wlk0prc  29738  wlksoneq1eq2  29748  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  crctcshlem4  29905  crctcsh  29909  wlkiswwlks1  29952  wwlksnext  29978  wwlksnextbi  29979  wwlksnextwrd  29982  midwwlks2s3  30037  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2a4  30084  clwlkclwwlklem3  30088  clwwisshclwws  30102  erclwwlkeqlen  30106  clwwlkinwwlk  30127  clwwlkn2  30131  clwwlkf  30134  clwwlkf1  30136  eleclclwwlknlem2  30148  erclwwlkneqlen  30155  umgrhashecclwwlk  30165  eucrctshift  30330  eucrct2eupth  30332  fusgr2wsp2nb  30421  grpoidinvlem2  30593  vcz  30663  nvz  30757  lnon0  30886  ipasslem2  30920  htthlem  31005  hvpncan  31127  hiidge0  31186  normgt0  31215  hsn0elch  31336  shsel3  31403  spansneleq  31658  normcan  31664  h1datomi  31669  fh1  31706  spansncvi  31740  5oalem1  31742  5oalem3  31744  5oalem5  31746  3oalem2  31751  pjdsi  31800  kbpj  32044  0hmop  32071  0lnfn  32073  adj0  32082  nlelshi  32148  branmfn  32193  opsqrlem1  32228  hst1h  32315  mdsl0  32398  superpos  32442  sumdmdlem  32506  cdj3lem1  32522  f1od2  32809  xrpxdivcld  33027  xrge0npcan  33113  elrgspnlem2  33337  rlocf1  33367  resvid2  33423  resvval2  33424  qsdrng  33590  r1pquslmic  33704  mplvrpmmhm  33723  mplvrpmrhm  33724  esplyfval0  33741  esplyfvaln  33751  vietalem  33756  rtelextdg2lem  33904  esumsnf  34242  esummulc1  34259  measxun2  34388  omsmeas  34501  sibfof  34518  probun  34597  signstfvn  34747  bnj517  35061  pthhashvtx  35344  ex-sategoelel  35637  mrsubfval  35724  msrval  35754  dfrdg2  36009  itgeq12i  36422  bj-prmoore  37368  bj-bary1lem1  37566  rdgeqoa  37625  finxpreclem2  37645  finxpreclem3  37648  matunitlindflem1  37867  poimirlem1  37872  poimirlem2  37873  poimirlem3  37874  poimirlem4  37875  poimirlem5  37876  poimirlem6  37877  poimirlem7  37878  poimirlem10  37881  poimirlem11  37882  poimirlem12  37883  poimirlem14  37885  poimirlem15  37886  poimirlem17  37888  poimirlem20  37891  poimirlem22  37893  poimirlem23  37894  poimirlem24  37895  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  mblfinlem2  37909  mblfinlem3  37910  ismblfin  37912  mbfposadd  37918  itg2addnclem  37922  itg2addnclem3  37924  itg2addnc  37925  ftc1anclem8  37951  areacirc  37964  ismtyval  38051  ismrer1  38089  grposnOLD  38133  rabeq12f  38408  csbeq12  38409  iuneq12f  38414  lsatcv1  39424  glbconN  39753  atltcvr  39811  3dim2  39844  islln2a  39893  2at0mat0  39901  islpln2a  39924  islvol2aN  39968  pmodlem2  40223  pmapjat1  40229  pcl0bN  40299  osumclN  40343  pexmidALTN  40354  lhp2at0nle  40411  4atexlemunv  40442  cdleme18b  40668  cdleme31sn1  40757  cdleme31sde  40761  cdleme31sn2  40765  ltrniotavalbN  40960  trljco  41116  cdlemh  41193  cdlemk40t  41294  cdlemk40f  41295  cdleml9  41360  dihmeetlem3N  41681  dochkrshp  41762  dihprrn  41802  dihjat1  41805  dvh3dim  41822  dochkrsm  41834  dochexmid  41844  lcfl7lem  41875  lcfl9a  41881  lclkrlem1  41882  mapdspex  42044  mapdindp2  42097  mapdh6dN  42115  hdmap1l6d  42189  hdmap11lem2  42218  hdmap14lem4a  42247  hdmapip0  42291  hlhilset  42310  nnadd1com  42637  mulgt0b2d  42848  fiabv  42906  prjspner1  42984  0prjspnrel  42985  jm2.26a  43357  onov0suclim  43631  oe0suclim  43634  cantnfresb  43681  onmcl  43688  omcl2  43690  tfsconcatun  43694  naddwordnexlem4  43758  mnringmulrcld  44584  radcnvrat  44670  sumsnd  45386  icccncfext  46245  fperdvper  46277  dvcosax  46284  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  volioc  46330  itgiccshift  46338  stoweidlem34  46392  dirkercncflem2  46462  fourierdlem32  46497  fourierdlem41  46506  fourierdlem48  46512  fourierdlem64  46528  fourierdlem73  46537  fourierdlem79  46543  fourierdlem82  46546  fourierdlem97  46561  fourierdlem101  46565  fourierdlem109  46573  fourierdlem111  46575  fouriersw  46589  elaa2  46592  etransclem24  46616  etransclem25  46617  etransclem46  46638  nnfoctbdjlem  46813  ismeannd  46825  smfpimltxr  47105  smfpimgtxr  47138  ndfatafv2undef  47572  fzopredsuc  47683  m1modmmod  47718  modlt0b  47723  prproropf1olem3  47865  prproropf1olem4  47866  fmtnorec2lem  47902  2pwp1prmfmtno  47950  sfprmdvdsmersenne  47963  sgprmdvdsmersenne  47964  lighneallem2  47966  lighneallem3  47967  dfodd6  47997  dfeven4  47998  m1expevenALTV  48007  isubgredg  48226  upgrimwlklem5  48261  gricushgr  48277  stgrusgra  48319  isubgr3stgrlem8  48333  clintopval  48564  lmod0rng  48589  zlidlring  48594  2zrngagrp  48609  dmmpossx2  48697  zlmodzxzscm  48717  zlmodzxzadd  48718  domnmsuppn0  48729  rmsuppss  48730  scmsuppss  48731  ply1mulgsumlem4  48749  ldepsprlem  48832  lincresunit2  48838  nn0sumshdiglemB  48980  2arymptfv  49010  ackval42  49056  affinecomb1  49062  itschlc0yqe  49120  itsclquadb  49136  2itscp  49141  incat  49960  0setrec  50063