Theorem sylan9eqr 2793

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 2791	. 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 2708

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

This theorem is referenced by:  sbcied2  3773  csbied2  3874  opthhausdorff0  5472  fun2ssres  6543  fcoi1  6714  fcoi2  6715  funssfv  6861  fvtp1  7150  nvof1o  7235  onuninsuci  7791  ot1stg  7956  ot2ndg  7957  el2xptp0  7989  mpomptsx  8017  dmmpossx  8019  fmpox  8020  2ndconst  8051  offsplitfpar  8069  mpoxopoveq  8169  rdgeq12  8352  rdgsucmptnf  8368  frsucmptn  8378  oev2  8458  oesuclem  8460  oawordeulem  8489  om00  8510  omass  8515  omeulem1  8517  oeoa  8533  oeoe  8535  nnmass  8560  oaabs2  8585  omabs  8587  mapsnend  8983  omxpenlem  9016  sbthlem4  9028  sbthlem6  9030  fodomr  9066  ssenen  9089  fodomfir  9238  fi0  9333  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  11569  subdivcomb2  11851  nnadd1com  12200  nnnn0addcl  12467  zindd  12630  qaddcl  12915  qmulcl  12917  qreccl  12919  xaddnemnf  13188  xaddnepnf  13189  xaddcom  13192  xnegdi  13200  xaddass  13201  xpncan  13203  xleadd1a  13205  xlt2add  13212  rexmul  13223  xmulgt0  13235  xmulge0  13236  xmulasslem3  13238  xlemul1a  13240  xadddilem  13246  xadddi2  13249  modmuladd  13875  modm1p1mod0  13884  modfzo0difsn  13905  seqf1olem2  14004  expp1  14030  expneg  14031  expcllem  14034  mulexp  14063  expmul  14069  sqoddm1div8  14205  bcpasc  14283  hashrabsn01  14335  fseq1hash  14338  hashinfxadd  14347  hashfzo  14391  fnfz0hash  14408  ffzo0hash  14411  hashf1lem1  14417  hashge2el2dif  14442  hash3tpexb  14456  hashdifsnp1  14468  lsw0  14527  ccatval1  14539  ccatval2  14540  swrdval  14606  ccatopth  14678  reuccatpfxs1  14709  splval  14713  repswswrd  14746  2cshwcshw  14787  s4dom  14881  wrdlen2i  14904  shftfn  15035  reim0b  15081  cjexp  15112  sqeqd  15128  fsumser  15692  sumsnf  15705  binomlem  15794  expcnv  15829  prodsn  15927  prodsnf  15929  bpolylem  16013  bpoly2  16022  bpoly3  16023  ef0lem  16043  dvdsnegb  16242  mod2eq1n2dvds  16316  m1expe  16343  m1expo  16344  m1exp1  16345  flodddiv4  16384  sadadd2lem2  16419  bezoutr1  16538  dvdslcm  16567  lcmeq0  16569  lcmcl  16570  lcmabs  16574  lcmgcdlem  16575  lcmdvds  16577  lcmf0val  16591  lcmftp  16605  lcmfunsnlem2  16609  mulgcddvds  16624  divgcdcoprmex  16635  pcge0  16833  pcadd  16860  pcmpt2  16864  prmreclem4  16890  ramval  16979  ramcl  17000  fvprmselelfz  17015  fvprmselgcd1  17016  ressid2  17204  ressval2  17205  mndind  18796  frmdval  18819  efmnd  18838  smndex1igid  18874  smndex1igidOLD  18875  smndex1n0mnd  18883  mgm2nsgrplem3  18891  mulgfval  19045  mulgfvalALT  19046  mulgnn0subcl  19063  mulgnn0z  19077  cycsubm  19177  f1ghm0to0  19220  isga  19266  symgextfve  19394  symgfixf1  19412  f1omvdco2  19423  psgnsn  19495  odid  19513  gexid  19556  efgsval2  19708  frgpuptinv  19746  frgpup2  19751  dprdsn  20013  srgmulgass  20198  srgpcomp  20199  srgbinomlem4  20210  ringinvnzdiv  20282  rngcval  20595  ringcval  20624  isabvd  20789  issrng  20821  lmodvsmmulgdi  20892  mptscmfsupp0  20922  lvecinv  21111  lspdisj2  21125  lspfixed  21126  lspexch  21127  sralem  21171  srasca  21175  sravsca  21176  sraip  21177  znval  21515  psgndiflemB  21580  isphl  21608  assamulgscmlem2  21880  mplval  21967  opsrval  22024  psdmvr  22135  cply1mul  22261  gsummoncoe1  22273  evl1fval  22293  scmate  22475  scmatscm  22478  mdetdiagid  22565  mdetunilem7  22583  mdetuni0  22586  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  slesolinvbi  22646  cpmatacl  22681  cpmatinvcl  22682  pmatcollpw2lem  22742  monmatcollpw  22744  pmatcollpwfi  22747  mp2pm2mplem4  22774  pm2mp  22790  cpmadugsumlemF  22841  cpmadugsumfi  22842  cpmadumatpoly  22848  cayhamlem4  22853  cayleyhamilton0  22854  cayleyhamiltonALT  22856  indistopon  22966  0ntr  23036  pnrmopn  23308  reftr  23479  kgenval  23500  pt1hmeo  23771  fmval  23908  fmf  23910  istmd  24039  istgp  24042  tsmsval2  24095  isxmet2d  24292  xpsxmetlem  24344  xpsmet  24347  blfvalps  24348  tmsval  24446  isnlm  24640  nmoleub  24696  idnghm  24708  blssioo  24760  blcvx  24763  icccvx  24917  pcorevlem  24993  isclm  25031  caufval  25242  iscms  25312  mbfsup  25631  i1f1  25657  dvexp3  25945  rolle  25957  dvivth  25977  deg1add  26068  0dgr  26210  coefv0  26213  elqaalem2  26286  dvradcnv  26386  abelthlem8  26404  efper  26443  logtayl  26624  abscxpbnd  26717  relogbcxpb  26751  logbgcd1irr  26758  dcubic2  26808  rlimcnp2  26930  cvxcl  26948  zetacvg  26978  lgamgulmlem2  26993  vmaval  27076  chtub  27175  logexprlim  27188  dchrsum2  27231  sumdchr2  27233  bposlem2  27248  lgsdir  27295  lgsne0  27298  lgsdirnn0  27307  lgsdinn0  27308  lgsquadlem2  27344  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2sqn0  27397  dchrvmasum2if  27460  dchrvmasumiflem1  27464  rpvmasum2  27475  pntpbnd1  27549  ostth2lem4  27599  expsp1  28421  trgcgrg  28583  tgcgr4  28599  ax5seglem1  28997  ax5seglem2  28998  ax5seglem5  29002  usgr1vr  29324  cplgr2vpr  29502  cplgr3v  29504  cusgrrusgr  29650  wlklenvm1  29690  wlk0prc  29721  wlksoneq1eq2  29731  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  crctcshlem4  29888  crctcsh  29892  wlkiswwlks1  29935  wwlksnext  29961  wwlksnextbi  29962  wwlksnextwrd  29965  midwwlks2s3  30020  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2a4  30067  clwlkclwwlklem3  30071  clwwisshclwws  30085  erclwwlkeqlen  30089  clwwlkinwwlk  30110  clwwlkn2  30114  clwwlkf  30117  clwwlkf1  30119  eleclclwwlknlem2  30131  erclwwlkneqlen  30138  umgrhashecclwwlk  30148  eucrctshift  30313  eucrct2eupth  30315  fusgr2wsp2nb  30404  grpoidinvlem2  30576  vcz  30646  nvz  30740  lnon0  30869  ipasslem2  30903  htthlem  30988  hvpncan  31110  hiidge0  31169  normgt0  31198  hsn0elch  31319  shsel3  31386  spansneleq  31641  normcan  31647  h1datomi  31652  fh1  31689  spansncvi  31723  5oalem1  31725  5oalem3  31727  5oalem5  31729  3oalem2  31734  pjdsi  31783  kbpj  32027  0hmop  32054  0lnfn  32056  adj0  32065  nlelshi  32131  branmfn  32176  opsqrlem1  32211  hst1h  32298  mdsl0  32381  superpos  32425  sumdmdlem  32489  cdj3lem1  32505  f1od2  32792  xrpxdivcld  32994  xrge0npcan  33080  elrgspnlem2  33304  rlocf1  33334  resvid2  33390  resvval2  33391  qsdrng  33557  r1pquslmic  33671  mplvrpmmhm  33690  mplvrpmrhm  33691  esplyfval0  33708  esplyfvaln  33718  vietalem  33723  rtelextdg2lem  33870  esumsnf  34208  esummulc1  34225  measxun2  34354  omsmeas  34467  sibfof  34484  probun  34563  signstfvn  34713  bnj517  35027  pthhashvtx  35310  ex-sategoelel  35603  mrsubfval  35690  msrval  35720  dfrdg2  35975  itgeq12i  36388  bj-prmoore  37427  bj-bary1lem1  37625  rdgeqoa  37686  finxpreclem2  37706  finxpreclem3  37709  matunitlindflem1  37937  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem14  37955  poimirlem15  37956  poimirlem17  37958  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  mblfinlem2  37979  mblfinlem3  37980  ismblfin  37982  mbfposadd  37988  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  ftc1anclem8  38021  areacirc  38034  ismtyval  38121  ismrer1  38159  grposnOLD  38203  rabeq12f  38478  csbeq12  38479  iuneq12f  38484  lsatcv1  39494  glbconN  39823  atltcvr  39881  3dim2  39914  islln2a  39963  2at0mat0  39971  islpln2a  39994  islvol2aN  40038  pmodlem2  40293  pmapjat1  40299  pcl0bN  40369  osumclN  40413  pexmidALTN  40424  lhp2at0nle  40481  4atexlemunv  40512  cdleme18b  40738  cdleme31sn1  40827  cdleme31sde  40831  cdleme31sn2  40835  ltrniotavalbN  41030  trljco  41186  cdlemh  41263  cdlemk40t  41364  cdlemk40f  41365  cdleml9  41430  dihmeetlem3N  41751  dochkrshp  41832  dihprrn  41872  dihjat1  41875  dvh3dim  41892  dochkrsm  41904  dochexmid  41914  lcfl7lem  41945  lcfl9a  41951  lclkrlem1  41952  mapdspex  42114  mapdindp2  42167  mapdh6dN  42185  hdmap1l6d  42259  hdmap11lem2  42288  hdmap14lem4a  42317  hdmapip0  42361  hlhilset  42380  mulgt0b2d  42923  fiabv  42981  prjspner1  43059  0prjspnrel  43060  jm2.26a  43428  onov0suclim  43702  oe0suclim  43705  cantnfresb  43752  onmcl  43759  omcl2  43761  tfsconcatun  43765  naddwordnexlem4  43829  mnringmulrcld  44655  radcnvrat  44741  sumsnd  45457  icccncfext  46315  fperdvper  46347  dvcosax  46354  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  volioc  46400  itgiccshift  46408  stoweidlem34  46462  dirkercncflem2  46532  fourierdlem32  46567  fourierdlem41  46576  fourierdlem48  46582  fourierdlem64  46598  fourierdlem73  46607  fourierdlem79  46613  fourierdlem82  46616  fourierdlem97  46631  fourierdlem101  46635  fourierdlem109  46643  fourierdlem111  46645  fouriersw  46659  elaa2  46662  etransclem24  46686  etransclem25  46687  etransclem46  46708  nnfoctbdjlem  46883  ismeannd  46895  smfpimltxr  47175  smfpimgtxr  47208  ndfatafv2undef  47660  fzopredsuc  47772  m1modmmod  47812  modlt0b  47817  prproropf1olem3  47965  prproropf1olem4  47966  fmtnorec2lem  48005  2pwp1prmfmtno  48053  sfprmdvdsmersenne  48066  sgprmdvdsmersenne  48067  lighneallem2  48069  lighneallem3  48070  ppivalnnprm  48088  ppivalnnnprmge6  48089  dfodd6  48113  dfeven4  48114  m1expevenALTV  48123  isubgredg  48342  upgrimwlklem5  48377  gricushgr  48393  stgrusgra  48435  isubgr3stgrlem8  48449  clintopval  48680  lmod0rng  48705  zlidlring  48710  2zrngagrp  48725  dmmpossx2  48813  zlmodzxzscm  48833  zlmodzxzadd  48834  domnmsuppn0  48845  rmsuppss  48846  scmsuppss  48847  ply1mulgsumlem4  48865  ldepsprlem  48948  lincresunit2  48954  nn0sumshdiglemB  49096  2arymptfv  49126  ackval42  49172  affinecomb1  49178  itschlc0yqe  49236  itsclquadb  49252  2itscp  49257  incat  50076  0setrec  50179