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 462	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2726

This theorem is referenced by:  sbcied2  3734  csbied2  3842  opthhausdorff0  5390  fun2ssres  6414  fcoi1  6582  fcoi2  6583  funssfv  6727  fvtp1  6999  nvof1o  7080  onuninsuci  7608  ot1stg  7764  ot2ndg  7765  el2xptp0  7797  mpomptsx  7823  dmmpossx  7825  fmpox  7826  2ndconst  7858  offsplitfpar  7877  mpoxopoveq  7950  wfrlem10  8053  rdgeq12  8138  rdgsucmptnf  8154  frsucmptn  8163  oev2  8239  oesuclem  8241  oawordeulem  8271  om00  8292  omass  8297  omeulem1  8299  oeoa  8314  oeoe  8316  nnmass  8341  oaabs2  8363  omabs  8365  mapsnend  8702  omxpenlem  8735  sbthlem4  8748  sbthlem6  8750  fodomr  8786  ssenen  8809  fi0  9025  cantnfp1  9285  cnfcomlem  9303  cardaleph  9686  cflim2  9860  axdc4lem  10052  fpwwe2lem11  10238  fpwwe2lem12  10239  rankcf  10374  inatsk  10375  ltrnq  10576  addclprlem1  10613  mulclprlem  10616  1idpr  10626  prlem936  10644  reclem3pr  10646  mulcmpblnrlem  10667  recexsrlem  10700  map2psrpr  10707  addid0  11234  subdivcomb2  11511  nnnn0addcl  12103  zindd  12261  qaddcl  12544  qmulcl  12546  qreccl  12548  xaddnemnf  12809  xaddnepnf  12810  xaddcom  12813  xnegdi  12821  xaddass  12822  xpncan  12824  xleadd1a  12826  xlt2add  12833  rexmul  12844  xmulgt0  12856  xmulge0  12857  xmulasslem3  12859  xlemul1a  12861  xadddilem  12867  xadddi2  12870  modmuladd  13469  modm1p1mod0  13478  modfzo0difsn  13499  seqf1olem2  13599  expp1  13625  expneg  13626  expcllem  13629  mulexp  13657  expmul  13663  sqoddm1div8  13793  bcpasc  13870  hashrabsn01  13923  fseq1hash  13926  hashinfxadd  13935  hashfzo  13979  fnfz0hash  13993  ffzo0hash  13996  hashf1lem1  14003  hashf1lem1OLD  14004  hashge2el2dif  14029  hashdifsnp1  14045  lsw0  14103  ccatval1  14116  ccatval1OLD  14117  ccatval2  14118  swrdval  14191  ccatopth  14264  reuccatpfxs1  14295  splval  14299  repswswrd  14332  2cshwcshw  14373  s4dom  14467  wrdlen2i  14490  shftfn  14619  reim0b  14665  cjexp  14696  sqeqd  14712  fsumser  15277  sumsnf  15289  binomlem  15374  expcnv  15409  prodsn  15505  prodsnf  15507  bpolylem  15591  bpoly2  15600  bpoly3  15601  ef0lem  15621  dvdsnegb  15816  mod2eq1n2dvds  15889  m1expe  15916  m1expo  15917  m1exp1  15918  flodddiv4  15955  sadadd2lem2  15990  gcdabsOLD  16072  bezoutr1  16107  dvdslcm  16136  lcmeq0  16138  lcmcl  16139  lcmabs  16143  lcmgcdlem  16144  lcmdvds  16146  lcmf0val  16160  lcmftp  16174  lcmfunsnlem2  16178  mulgcddvds  16193  divgcdcoprmex  16204  pcge0  16396  pcadd  16423  pcmpt2  16427  prmreclem4  16453  ramval  16542  ramcl  16563  fvprmselelfz  16578  fvprmselgcd1  16579  ressid2  16754  ressval2  16755  mndind  18226  frmdval  18250  efmnd  18269  smndex1igid  18303  smndex1n0mnd  18311  mgm2nsgrplem3  18319  mulgfval  18462  mulgfvalALT  18463  mulgnn0subcl  18477  mulgnn0z  18490  cycsubm  18581  isga  18657  symgextfve  18783  symgfixf1  18801  f1omvdco2  18812  psgnsn  18884  odid  18902  gexid  18942  efgsval2  19095  frgpuptinv  19133  frgpup2  19138  dprdsn  19395  srgmulgass  19518  srgpcomp  19519  srgbinomlem4  19530  ringinvnzdiv  19583  f1ghm0to0  19732  f1rhm0to0ALT  19733  isabvd  19828  issrng  19858  lmodvsmmulgdi  19906  mptscmfsupp0  19936  lvecinv  20122  lspdisj2  20136  lspfixed  20137  lspexch  20138  sralem  20186  srasca  20190  sravsca  20191  sraip  20192  znval  20472  psgndiflemB  20534  isphl  20562  assamulgscmlem2  20832  mplval  20925  opsrval  20975  cply1mul  21187  gsummoncoe1  21197  evl1fval  21216  scmate  21379  scmatscm  21382  mdetdiagid  21469  mdetunilem7  21487  mdetuni0  21490  gsummatr01lem3  21526  gsummatr01lem4  21527  gsummatr01  21528  slesolinvbi  21550  cpmatacl  21585  cpmatinvcl  21586  pmatcollpw2lem  21646  monmatcollpw  21648  pmatcollpwfi  21651  mp2pm2mplem4  21678  pm2mp  21694  cpmadugsumlemF  21745  cpmadugsumfi  21746  cpmadumatpoly  21752  cayhamlem4  21757  cayleyhamilton0  21758  cayleyhamiltonALT  21760  indistopon  21870  0ntr  21940  pnrmopn  22212  reftr  22383  kgenval  22404  pt1hmeo  22675  fmval  22812  fmf  22814  istmd  22943  istgp  22946  tsmsval2  22999  isxmet2d  23197  xpsxmetlem  23249  xpsmet  23252  blfvalps  23253  tmsval  23351  isnlm  23545  nmoleub  23601  idnghm  23613  blssioo  23664  blcvx  23667  icccvx  23819  pcorevlem  23895  isclm  23933  caufval  24144  iscms  24214  mbfsup  24533  i1f1  24559  dvexp3  24847  rolle  24859  dvivth  24879  deg1add  24973  0dgr  25111  coefv0  25114  elqaalem2  25185  dvradcnv  25285  abelthlem8  25303  efper  25341  logtayl  25520  abscxpbnd  25611  relogbcxpb  25642  logbgcd1irr  25649  dcubic2  25699  rlimcnp2  25821  cvxcl  25839  zetacvg  25869  lgamgulmlem2  25884  vmaval  25967  chtub  26065  logexprlim  26078  dchrsum2  26121  sumdchr2  26123  bposlem2  26138  lgsdir  26185  lgsne0  26188  lgsdirnn0  26197  lgsdinn0  26198  lgsquadlem2  26234  2lgslem3a  26249  2lgslem3b  26250  2lgslem3c  26251  2lgslem3d  26252  2lgslem3a1  26253  2lgslem3b1  26254  2lgslem3c1  26255  2lgslem3d1  26256  2sqn0  26287  dchrvmasum2if  26350  dchrvmasumiflem1  26354  rpvmasum2  26365  pntpbnd1  26439  ostth2lem4  26489  trgcgrg  26578  tgcgr4  26594  ax5seglem1  26991  ax5seglem2  26992  ax5seglem5  26996  usgr1vr  27315  cplgr2vpr  27493  cplgr3v  27495  cusgrrusgr  27641  wlklenvm1  27681  wlk0prc  27713  wlksoneq1eq2  27724  crctcshwlkn0lem4  27869  crctcshwlkn0lem5  27870  crctcshwlkn0lem6  27871  crctcshlem4  27876  crctcsh  27880  wlkiswwlks1  27923  wwlksnext  27949  wwlksnextbi  27950  wwlksnextwrd  27953  midwwlks2s3  28008  clwlkclwwlklem2fv1  28050  clwlkclwwlklem2a4  28052  clwlkclwwlklem3  28056  clwwisshclwws  28070  erclwwlkeqlen  28074  clwwlkinwwlk  28095  clwwlkn2  28099  clwwlkf  28102  clwwlkf1  28104  eleclclwwlknlem2  28116  erclwwlkneqlen  28123  umgrhashecclwwlk  28133  eucrctshift  28298  eucrct2eupth  28300  fusgr2wsp2nb  28389  grpoidinvlem2  28558  vcz  28628  nvz  28722  lnon0  28851  ipasslem2  28885  htthlem  28970  hvpncan  29092  hiidge0  29151  normgt0  29180  hsn0elch  29301  shsel3  29368  spansneleq  29623  normcan  29629  h1datomi  29634  fh1  29671  spansncvi  29705  5oalem1  29707  5oalem3  29709  5oalem5  29711  3oalem2  29716  pjdsi  29765  kbpj  30009  0hmop  30036  0lnfn  30038  adj0  30047  nlelshi  30113  branmfn  30158  opsqrlem1  30193  hst1h  30280  mdsl0  30363  superpos  30407  sumdmdlem  30471  cdj3lem1  30487  f1od2  30748  xrpxdivcld  30901  xrge0npcan  30994  resvid2  31218  resvval2  31219  esumsnf  31716  esummulc1  31733  measxun2  31862  omsmeas  31974  sibfof  31991  probun  32070  signstfvn  32232  bnj517  32550  pthhashvtx  32774  ex-sategoelel  33068  mrsubfval  33155  msrval  33185  dfrdg2  33459  bj-prmoore  34978  bj-bary1lem1  35173  rdgeqoa  35235  finxpreclem2  35255  finxpreclem3  35258  matunitlindflem1  35467  poimirlem1  35472  poimirlem2  35473  poimirlem3  35474  poimirlem4  35475  poimirlem5  35476  poimirlem6  35477  poimirlem7  35478  poimirlem10  35481  poimirlem11  35482  poimirlem12  35483  poimirlem14  35485  poimirlem15  35486  poimirlem17  35488  poimirlem20  35491  poimirlem22  35493  poimirlem23  35494  poimirlem24  35495  poimirlem25  35496  poimirlem26  35497  poimirlem27  35498  mblfinlem2  35509  mblfinlem3  35510  ismblfin  35512  mbfposadd  35518  itg2addnclem  35522  itg2addnclem3  35524  itg2addnc  35525  ftc1anclem8  35551  areacirc  35564  ismtyval  35652  ismrer1  35690  grposnOLD  35734  rabeq12f  36009  csbeq12  36010  iuneq12f  36015  lsatcv1  36756  glbconN  37085  atltcvr  37143  3dim2  37176  islln2a  37225  2at0mat0  37233  islpln2a  37256  islvol2aN  37300  pmodlem2  37555  pmapjat1  37561  pcl0bN  37631  osumclN  37675  pexmidALTN  37686  lhp2at0nle  37743  4atexlemunv  37774  cdleme18b  38000  cdleme31sn1  38089  cdleme31sde  38093  cdleme31sn2  38097  ltrniotavalbN  38292  trljco  38448  cdlemh  38525  cdlemk40t  38626  cdlemk40f  38627  cdleml9  38692  dihmeetlem3N  39013  dochkrshp  39094  dihprrn  39134  dihjat1  39137  dvh3dim  39154  dochkrsm  39166  dochexmid  39176  lcfl7lem  39207  lcfl9a  39213  lclkrlem1  39214  mapdspex  39376  mapdindp2  39429  mapdh6dN  39447  hdmap1l6d  39521  hdmap11lem2  39550  hdmap14lem4a  39579  hdmapip0  39623  hlhilset  39642  nnadd1com  39956  sn-negex12  40058  prjspner1  40123  0prjspnrel  40124  jm2.26a  40477  mnringmulrcld  41471  radcnvrat  41557  sumsnd  42194  icccncfext  43057  fperdvper  43089  dvcosax  43096  ioodvbdlimc1lem1  43101  ioodvbdlimc1lem2  43102  ioodvbdlimc2lem  43104  volioc  43142  itgiccshift  43150  stoweidlem34  43204  dirkercncflem2  43274  fourierdlem32  43309  fourierdlem41  43318  fourierdlem48  43324  fourierdlem64  43340  fourierdlem73  43349  fourierdlem79  43355  fourierdlem82  43358  fourierdlem97  43373  fourierdlem101  43377  fourierdlem109  43385  fourierdlem111  43387  fouriersw  43401  elaa2  43404  etransclem24  43428  etransclem25  43429  etransclem46  43450  nnfoctbdjlem  43622  ismeannd  43634  ndfatafv2undef  44330  fzopredsuc  44442  prproropf1olem3  44584  prproropf1olem4  44585  fmtnorec2lem  44621  2pwp1prmfmtno  44669  sfprmdvdsmersenne  44682  sgprmdvdsmersenne  44683  lighneallem2  44685  lighneallem3  44686  dfodd6  44716  dfeven4  44717  m1expevenALTV  44726  isomushgr  44905  isomuspgrlem2d  44910  clintopval  45025  lmod0rng  45053  zlidlring  45113  2zrngagrp  45128  rngcval  45147  ringcval  45193  dmmpossx2  45299  zlmodzxzscm  45320  zlmodzxzadd  45321  domnmsuppn0  45332  rmsuppss  45333  scmsuppss  45335  ply1mulgsumlem4  45357  ldepsprlem  45440  lincresunit2  45446  m1modmmod  45494  nn0sumshdiglemB  45593  2arymptfv  45623  ackval42  45669  affinecomb1  45675  itschlc0yqe  45733  itsclquadb  45749  2itscp  45754  0setrec  46034