Theorem sylan9eqr 2788

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  sbcied2  3786  csbied2  3887  opthhausdorff0  5458  fun2ssres  6526  fcoi1  6697  fcoi2  6698  funssfv  6843  fvtp1  7129  nvof1o  7214  onuninsuci  7770  ot1stg  7935  ot2ndg  7936  el2xptp0  7968  mpomptsx  7996  dmmpossx  7998  fmpox  7999  2ndconst  8031  offsplitfpar  8049  mpoxopoveq  8149  rdgeq12  8332  rdgsucmptnf  8348  frsucmptn  8358  oev2  8438  oesuclem  8440  oawordeulem  8469  om00  8490  omass  8495  omeulem1  8497  oeoa  8512  oeoe  8514  nnmass  8539  oaabs2  8564  omabs  8566  mapsnend  8958  omxpenlem  8991  sbthlem4  9003  sbthlem6  9005  fodomr  9041  ssenen  9064  fodomfir  9212  fi0  9304  cantnfp1  9571  cnfcomlem  9589  ttrclselem2  9616  cardaleph  9980  cflim2  10154  axdc4lem  10346  fpwwe2lem11  10532  fpwwe2lem12  10533  rankcf  10668  inatsk  10669  ltrnq  10870  addclprlem1  10907  mulclprlem  10910  1idpr  10920  prlem936  10938  reclem3pr  10940  mulcmpblnrlem  10961  recexsrlem  10994  map2psrpr  11001  addid0  11536  subdivcomb2  11817  nnnn0addcl  12411  zindd  12574  qaddcl  12863  qmulcl  12865  qreccl  12867  xaddnemnf  13135  xaddnepnf  13136  xaddcom  13139  xnegdi  13147  xaddass  13148  xpncan  13150  xleadd1a  13152  xlt2add  13159  rexmul  13170  xmulgt0  13182  xmulge0  13183  xmulasslem3  13185  xlemul1a  13187  xadddilem  13193  xadddi2  13196  modmuladd  13820  modm1p1mod0  13829  modfzo0difsn  13850  seqf1olem2  13949  expp1  13975  expneg  13976  expcllem  13979  mulexp  14008  expmul  14014  sqoddm1div8  14150  bcpasc  14228  hashrabsn01  14280  fseq1hash  14283  hashinfxadd  14292  hashfzo  14336  fnfz0hash  14353  ffzo0hash  14356  hashf1lem1  14362  hashge2el2dif  14387  hash3tpexb  14401  hashdifsnp1  14413  lsw0  14472  ccatval1  14484  ccatval2  14485  swrdval  14551  ccatopth  14623  reuccatpfxs1  14654  splval  14658  repswswrd  14691  2cshwcshw  14732  s4dom  14826  wrdlen2i  14849  shftfn  14980  reim0b  15026  cjexp  15057  sqeqd  15073  fsumser  15637  sumsnf  15650  binomlem  15736  expcnv  15771  prodsn  15869  prodsnf  15871  bpolylem  15955  bpoly2  15964  bpoly3  15965  ef0lem  15985  dvdsnegb  16184  mod2eq1n2dvds  16258  m1expe  16285  m1expo  16286  m1exp1  16287  flodddiv4  16326  sadadd2lem2  16361  bezoutr1  16480  dvdslcm  16509  lcmeq0  16511  lcmcl  16512  lcmabs  16516  lcmgcdlem  16517  lcmdvds  16519  lcmf0val  16533  lcmftp  16547  lcmfunsnlem2  16551  mulgcddvds  16566  divgcdcoprmex  16577  pcge0  16774  pcadd  16801  pcmpt2  16805  prmreclem4  16831  ramval  16920  ramcl  16941  fvprmselelfz  16956  fvprmselgcd1  16957  ressid2  17145  ressval2  17146  mndind  18736  frmdval  18759  efmnd  18778  smndex1igid  18812  smndex1n0mnd  18820  mgm2nsgrplem3  18828  mulgfval  18982  mulgfvalALT  18983  mulgnn0subcl  19000  mulgnn0z  19014  cycsubm  19115  f1ghm0to0  19158  isga  19204  symgextfve  19332  symgfixf1  19350  f1omvdco2  19361  psgnsn  19433  odid  19451  gexid  19494  efgsval2  19646  frgpuptinv  19684  frgpup2  19689  dprdsn  19951  srgmulgass  20136  srgpcomp  20137  srgbinomlem4  20148  ringinvnzdiv  20220  rngcval  20534  ringcval  20563  isabvd  20728  issrng  20760  lmodvsmmulgdi  20831  mptscmfsupp0  20861  lvecinv  21051  lspdisj2  21065  lspfixed  21066  lspexch  21067  sralem  21111  srasca  21115  sravsca  21116  sraip  21117  znval  21473  psgndiflemB  21538  isphl  21566  assamulgscmlem2  21838  mplval  21927  opsrval  21982  psdmvr  22085  cply1mul  22212  gsummoncoe1  22224  evl1fval  22244  scmate  22426  scmatscm  22429  mdetdiagid  22516  mdetunilem7  22534  mdetuni0  22537  gsummatr01lem3  22573  gsummatr01lem4  22574  gsummatr01  22575  slesolinvbi  22597  cpmatacl  22632  cpmatinvcl  22633  pmatcollpw2lem  22693  monmatcollpw  22695  pmatcollpwfi  22698  mp2pm2mplem4  22725  pm2mp  22741  cpmadugsumlemF  22792  cpmadugsumfi  22793  cpmadumatpoly  22799  cayhamlem4  22804  cayleyhamilton0  22805  cayleyhamiltonALT  22807  indistopon  22917  0ntr  22987  pnrmopn  23259  reftr  23430  kgenval  23451  pt1hmeo  23722  fmval  23859  fmf  23861  istmd  23990  istgp  23993  tsmsval2  24046  isxmet2d  24243  xpsxmetlem  24295  xpsmet  24298  blfvalps  24299  tmsval  24397  isnlm  24591  nmoleub  24647  idnghm  24659  blssioo  24711  blcvx  24714  icccvx  24876  pcorevlem  24954  isclm  24992  caufval  25203  iscms  25273  mbfsup  25593  i1f1  25619  dvexp3  25910  rolle  25922  dvivth  25943  deg1add  26036  0dgr  26178  coefv0  26181  elqaalem2  26256  dvradcnv  26358  abelthlem8  26377  efper  26416  logtayl  26597  abscxpbnd  26691  relogbcxpb  26725  logbgcd1irr  26732  dcubic2  26782  rlimcnp2  26904  cvxcl  26923  zetacvg  26953  lgamgulmlem2  26968  vmaval  27051  chtub  27151  logexprlim  27164  dchrsum2  27207  sumdchr2  27209  bposlem2  27224  lgsdir  27271  lgsne0  27274  lgsdirnn0  27283  lgsdinn0  27284  lgsquadlem2  27320  2lgslem3a  27335  2lgslem3b  27336  2lgslem3c  27337  2lgslem3d  27338  2lgslem3a1  27339  2lgslem3b1  27340  2lgslem3c1  27341  2lgslem3d1  27342  2sqn0  27373  dchrvmasum2if  27436  dchrvmasumiflem1  27440  rpvmasum2  27451  pntpbnd1  27525  ostth2lem4  27575  expsp1  28353  trgcgrg  28494  tgcgr4  28510  ax5seglem1  28907  ax5seglem2  28908  ax5seglem5  28912  usgr1vr  29234  cplgr2vpr  29412  cplgr3v  29414  cusgrrusgr  29561  wlklenvm1  29601  wlk0prc  29632  wlksoneq1eq2  29642  crctcshwlkn0lem4  29792  crctcshwlkn0lem5  29793  crctcshwlkn0lem6  29794  crctcshlem4  29799  crctcsh  29803  wlkiswwlks1  29846  wwlksnext  29872  wwlksnextbi  29873  wwlksnextwrd  29876  midwwlks2s3  29931  clwlkclwwlklem2fv1  29973  clwlkclwwlklem2a4  29975  clwlkclwwlklem3  29979  clwwisshclwws  29993  erclwwlkeqlen  29997  clwwlkinwwlk  30018  clwwlkn2  30022  clwwlkf  30025  clwwlkf1  30027  eleclclwwlknlem2  30039  erclwwlkneqlen  30046  umgrhashecclwwlk  30056  eucrctshift  30221  eucrct2eupth  30223  fusgr2wsp2nb  30312  grpoidinvlem2  30483  vcz  30553  nvz  30647  lnon0  30776  ipasslem2  30810  htthlem  30895  hvpncan  31017  hiidge0  31076  normgt0  31105  hsn0elch  31226  shsel3  31293  spansneleq  31548  normcan  31554  h1datomi  31559  fh1  31596  spansncvi  31630  5oalem1  31632  5oalem3  31634  5oalem5  31636  3oalem2  31641  pjdsi  31690  kbpj  31934  0hmop  31961  0lnfn  31963  adj0  31972  nlelshi  32038  branmfn  32083  opsqrlem1  32118  hst1h  32205  mdsl0  32288  superpos  32332  sumdmdlem  32396  cdj3lem1  32412  f1od2  32700  xrpxdivcld  32913  xrge0npcan  32999  elrgspnlem2  33208  rlocf1  33238  resvid2  33293  resvval2  33294  qsdrng  33460  r1pquslmic  33569  mplvrpmmhm  33574  mplvrpmrhm  33575  rtelextdg2lem  33737  esumsnf  34075  esummulc1  34092  measxun2  34221  omsmeas  34334  sibfof  34351  probun  34430  signstfvn  34580  bnj517  34895  pthhashvtx  35170  ex-sategoelel  35463  mrsubfval  35550  msrval  35580  dfrdg2  35835  itgeq12i  36246  bj-prmoore  37155  bj-bary1lem1  37351  rdgeqoa  37410  finxpreclem2  37430  finxpreclem3  37433  matunitlindflem1  37662  poimirlem1  37667  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem14  37680  poimirlem15  37681  poimirlem17  37683  poimirlem20  37686  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  mblfinlem2  37704  mblfinlem3  37705  ismblfin  37707  mbfposadd  37713  itg2addnclem  37717  itg2addnclem3  37719  itg2addnc  37720  ftc1anclem8  37746  areacirc  37759  ismtyval  37846  ismrer1  37884  grposnOLD  37928  rabeq12f  38203  csbeq12  38204  iuneq12f  38209  lsatcv1  39093  glbconN  39422  atltcvr  39480  3dim2  39513  islln2a  39562  2at0mat0  39570  islpln2a  39593  islvol2aN  39637  pmodlem2  39892  pmapjat1  39898  pcl0bN  39968  osumclN  40012  pexmidALTN  40023  lhp2at0nle  40080  4atexlemunv  40111  cdleme18b  40337  cdleme31sn1  40426  cdleme31sde  40430  cdleme31sn2  40434  ltrniotavalbN  40629  trljco  40785  cdlemh  40862  cdlemk40t  40963  cdlemk40f  40964  cdleml9  41029  dihmeetlem3N  41350  dochkrshp  41431  dihprrn  41471  dihjat1  41474  dvh3dim  41491  dochkrsm  41503  dochexmid  41513  lcfl7lem  41544  lcfl9a  41550  lclkrlem1  41551  mapdspex  41713  mapdindp2  41766  mapdh6dN  41784  hdmap1l6d  41858  hdmap11lem2  41887  hdmap14lem4a  41916  hdmapip0  41960  hlhilset  41979  nnadd1com  42306  mulgt0b2d  42517  fiabv  42575  prjspner1  42665  0prjspnrel  42666  jm2.26a  43039  onov0suclim  43313  oe0suclim  43316  cantnfresb  43363  onmcl  43370  omcl2  43372  tfsconcatun  43376  naddwordnexlem4  43440  mnringmulrcld  44267  radcnvrat  44353  sumsnd  45069  icccncfext  45931  fperdvper  45963  dvcosax  45970  ioodvbdlimc1lem1  45975  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  volioc  46016  itgiccshift  46024  stoweidlem34  46078  dirkercncflem2  46148  fourierdlem32  46183  fourierdlem41  46192  fourierdlem48  46198  fourierdlem64  46214  fourierdlem73  46223  fourierdlem79  46229  fourierdlem82  46232  fourierdlem97  46247  fourierdlem101  46251  fourierdlem109  46259  fourierdlem111  46261  fouriersw  46275  elaa2  46278  etransclem24  46302  etransclem25  46303  etransclem46  46324  nnfoctbdjlem  46499  ismeannd  46511  smfpimltxr  46791  smfpimgtxr  46824  ndfatafv2undef  47249  fzopredsuc  47360  m1modmmod  47395  modlt0b  47400  prproropf1olem3  47542  prproropf1olem4  47543  fmtnorec2lem  47579  2pwp1prmfmtno  47627  sfprmdvdsmersenne  47640  sgprmdvdsmersenne  47641  lighneallem2  47643  lighneallem3  47644  dfodd6  47674  dfeven4  47675  m1expevenALTV  47684  isubgredg  47903  upgrimwlklem5  47938  gricushgr  47954  stgrusgra  47996  isubgr3stgrlem8  48010  clintopval  48241  lmod0rng  48266  zlidlring  48271  2zrngagrp  48286  dmmpossx2  48374  zlmodzxzscm  48394  zlmodzxzadd  48395  domnmsuppn0  48406  rmsuppss  48407  scmsuppss  48408  ply1mulgsumlem4  48427  ldepsprlem  48510  lincresunit2  48516  nn0sumshdiglemB  48658  2arymptfv  48688  ackval42  48734  affinecomb1  48740  itschlc0yqe  48798  itsclquadb  48814  2itscp  48819  incat  49639  0setrec  49742