Theorem sylan9eqr 2786

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 2784	. 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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  sbcied2  3798  csbied2  3899  opthhausdorff0  5478  fun2ssres  6561  fcoi1  6734  fcoi2  6735  funssfv  6879  fvtp1  7169  nvof1o  7255  onuninsuci  7816  ot1stg  7982  ot2ndg  7983  el2xptp0  8015  mpomptsx  8043  dmmpossx  8045  fmpox  8046  2ndconst  8080  offsplitfpar  8098  mpoxopoveq  8198  rdgeq12  8381  rdgsucmptnf  8397  frsucmptn  8407  oev2  8487  oesuclem  8489  oawordeulem  8518  om00  8539  omass  8544  omeulem1  8546  oeoa  8561  oeoe  8563  nnmass  8588  oaabs2  8613  omabs  8615  mapsnend  9007  omxpenlem  9042  sbthlem4  9054  sbthlem6  9056  fodomr  9092  ssenen  9115  fodomfir  9279  fi0  9371  cantnfp1  9634  cnfcomlem  9652  ttrclselem2  9679  cardaleph  10042  cflim2  10216  axdc4lem  10408  fpwwe2lem11  10594  fpwwe2lem12  10595  rankcf  10730  inatsk  10731  ltrnq  10932  addclprlem1  10969  mulclprlem  10972  1idpr  10982  prlem936  11000  reclem3pr  11002  mulcmpblnrlem  11023  recexsrlem  11056  map2psrpr  11063  addid0  11597  subdivcomb2  11878  nnnn0addcl  12472  zindd  12635  qaddcl  12924  qmulcl  12926  qreccl  12928  xaddnemnf  13196  xaddnepnf  13197  xaddcom  13200  xnegdi  13208  xaddass  13209  xpncan  13211  xleadd1a  13213  xlt2add  13220  rexmul  13231  xmulgt0  13243  xmulge0  13244  xmulasslem3  13246  xlemul1a  13248  xadddilem  13254  xadddi2  13257  modmuladd  13878  modm1p1mod0  13887  modfzo0difsn  13908  seqf1olem2  14007  expp1  14033  expneg  14034  expcllem  14037  mulexp  14066  expmul  14072  sqoddm1div8  14208  bcpasc  14286  hashrabsn01  14338  fseq1hash  14341  hashinfxadd  14350  hashfzo  14394  fnfz0hash  14411  ffzo0hash  14414  hashf1lem1  14420  hashge2el2dif  14445  hash3tpexb  14459  hashdifsnp1  14471  lsw0  14530  ccatval1  14542  ccatval2  14543  swrdval  14608  ccatopth  14681  reuccatpfxs1  14712  splval  14716  repswswrd  14749  2cshwcshw  14791  s4dom  14885  wrdlen2i  14908  shftfn  15039  reim0b  15085  cjexp  15116  sqeqd  15132  fsumser  15696  sumsnf  15709  binomlem  15795  expcnv  15830  prodsn  15928  prodsnf  15930  bpolylem  16014  bpoly2  16023  bpoly3  16024  ef0lem  16044  dvdsnegb  16243  mod2eq1n2dvds  16317  m1expe  16344  m1expo  16345  m1exp1  16346  flodddiv4  16385  sadadd2lem2  16420  bezoutr1  16539  dvdslcm  16568  lcmeq0  16570  lcmcl  16571  lcmabs  16575  lcmgcdlem  16576  lcmdvds  16578  lcmf0val  16592  lcmftp  16606  lcmfunsnlem2  16610  mulgcddvds  16625  divgcdcoprmex  16636  pcge0  16833  pcadd  16860  pcmpt2  16864  prmreclem4  16890  ramval  16979  ramcl  17000  fvprmselelfz  17015  fvprmselgcd1  17016  ressid2  17204  ressval2  17205  mndind  18755  frmdval  18778  efmnd  18797  smndex1igid  18831  smndex1n0mnd  18839  mgm2nsgrplem3  18847  mulgfval  19001  mulgfvalALT  19002  mulgnn0subcl  19019  mulgnn0z  19033  cycsubm  19134  f1ghm0to0  19177  isga  19223  symgextfve  19349  symgfixf1  19367  f1omvdco2  19378  psgnsn  19450  odid  19468  gexid  19511  efgsval2  19663  frgpuptinv  19701  frgpup2  19706  dprdsn  19968  srgmulgass  20126  srgpcomp  20127  srgbinomlem4  20138  ringinvnzdiv  20210  rngcval  20527  ringcval  20556  isabvd  20721  issrng  20753  lmodvsmmulgdi  20803  mptscmfsupp0  20833  lvecinv  21023  lspdisj2  21037  lspfixed  21038  lspexch  21039  sralem  21083  srasca  21087  sravsca  21088  sraip  21089  znval  21445  psgndiflemB  21509  isphl  21537  assamulgscmlem2  21809  mplval  21898  opsrval  21953  psdmvr  22056  cply1mul  22183  gsummoncoe1  22195  evl1fval  22215  scmate  22397  scmatscm  22400  mdetdiagid  22487  mdetunilem7  22505  mdetuni0  22508  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  slesolinvbi  22568  cpmatacl  22603  cpmatinvcl  22604  pmatcollpw2lem  22664  monmatcollpw  22666  pmatcollpwfi  22669  mp2pm2mplem4  22696  pm2mp  22712  cpmadugsumlemF  22763  cpmadugsumfi  22764  cpmadumatpoly  22770  cayhamlem4  22775  cayleyhamilton0  22776  cayleyhamiltonALT  22778  indistopon  22888  0ntr  22958  pnrmopn  23230  reftr  23401  kgenval  23422  pt1hmeo  23693  fmval  23830  fmf  23832  istmd  23961  istgp  23964  tsmsval2  24017  isxmet2d  24215  xpsxmetlem  24267  xpsmet  24270  blfvalps  24271  tmsval  24369  isnlm  24563  nmoleub  24619  idnghm  24631  blssioo  24683  blcvx  24686  icccvx  24848  pcorevlem  24926  isclm  24964  caufval  25175  iscms  25245  mbfsup  25565  i1f1  25591  dvexp3  25882  rolle  25894  dvivth  25915  deg1add  26008  0dgr  26150  coefv0  26153  elqaalem2  26228  dvradcnv  26330  abelthlem8  26349  efper  26388  logtayl  26569  abscxpbnd  26663  relogbcxpb  26697  logbgcd1irr  26704  dcubic2  26754  rlimcnp2  26876  cvxcl  26895  zetacvg  26925  lgamgulmlem2  26940  vmaval  27023  chtub  27123  logexprlim  27136  dchrsum2  27179  sumdchr2  27181  bposlem2  27196  lgsdir  27243  lgsne0  27246  lgsdirnn0  27255  lgsdinn0  27256  lgsquadlem2  27292  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  2sqn0  27345  dchrvmasum2if  27408  dchrvmasumiflem1  27412  rpvmasum2  27423  pntpbnd1  27497  ostth2lem4  27547  expsp1  28315  trgcgrg  28442  tgcgr4  28458  ax5seglem1  28855  ax5seglem2  28856  ax5seglem5  28860  usgr1vr  29182  cplgr2vpr  29360  cplgr3v  29362  cusgrrusgr  29509  wlklenvm1  29550  wlk0prc  29582  wlksoneq1eq2  29592  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  crctcshlem4  29750  crctcsh  29754  wlkiswwlks1  29797  wwlksnext  29823  wwlksnextbi  29824  wwlksnextwrd  29827  midwwlks2s3  29882  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2a4  29926  clwlkclwwlklem3  29930  clwwisshclwws  29944  erclwwlkeqlen  29948  clwwlkinwwlk  29969  clwwlkn2  29973  clwwlkf  29976  clwwlkf1  29978  eleclclwwlknlem2  29990  erclwwlkneqlen  29997  umgrhashecclwwlk  30007  eucrctshift  30172  eucrct2eupth  30174  fusgr2wsp2nb  30263  grpoidinvlem2  30434  vcz  30504  nvz  30598  lnon0  30727  ipasslem2  30761  htthlem  30846  hvpncan  30968  hiidge0  31027  normgt0  31056  hsn0elch  31177  shsel3  31244  spansneleq  31499  normcan  31505  h1datomi  31510  fh1  31547  spansncvi  31581  5oalem1  31583  5oalem3  31585  5oalem5  31587  3oalem2  31592  pjdsi  31641  kbpj  31885  0hmop  31912  0lnfn  31914  adj0  31923  nlelshi  31989  branmfn  32034  opsqrlem1  32069  hst1h  32156  mdsl0  32239  superpos  32283  sumdmdlem  32347  cdj3lem1  32363  f1od2  32644  xrpxdivcld  32855  xrge0npcan  32961  elrgspnlem2  33194  rlocf1  33224  resvid2  33302  resvval2  33303  qsdrng  33468  r1pquslmic  33576  rtelextdg2lem  33716  esumsnf  34054  esummulc1  34071  measxun2  34200  omsmeas  34314  sibfof  34331  probun  34410  signstfvn  34560  bnj517  34875  pthhashvtx  35115  ex-sategoelel  35408  mrsubfval  35495  msrval  35525  dfrdg2  35783  itgeq12i  36194  bj-prmoore  37103  bj-bary1lem1  37299  rdgeqoa  37358  finxpreclem2  37378  finxpreclem3  37381  matunitlindflem1  37610  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem14  37628  poimirlem15  37629  poimirlem17  37631  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  mblfinlem2  37652  mblfinlem3  37653  ismblfin  37655  mbfposadd  37661  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem8  37694  areacirc  37707  ismtyval  37794  ismrer1  37832  grposnOLD  37876  rabeq12f  38151  csbeq12  38152  iuneq12f  38157  lsatcv1  39041  glbconN  39370  glbconNOLD  39371  atltcvr  39429  3dim2  39462  islln2a  39511  2at0mat0  39519  islpln2a  39542  islvol2aN  39586  pmodlem2  39841  pmapjat1  39847  pcl0bN  39917  osumclN  39961  pexmidALTN  39972  lhp2at0nle  40029  4atexlemunv  40060  cdleme18b  40286  cdleme31sn1  40375  cdleme31sde  40379  cdleme31sn2  40383  ltrniotavalbN  40578  trljco  40734  cdlemh  40811  cdlemk40t  40912  cdlemk40f  40913  cdleml9  40978  dihmeetlem3N  41299  dochkrshp  41380  dihprrn  41420  dihjat1  41423  dvh3dim  41440  dochkrsm  41452  dochexmid  41462  lcfl7lem  41493  lcfl9a  41499  lclkrlem1  41500  mapdspex  41662  mapdindp2  41715  mapdh6dN  41733  hdmap1l6d  41807  hdmap11lem2  41836  hdmap14lem4a  41865  hdmapip0  41909  hlhilset  41928  nnadd1com  42255  mulgt0b2d  42466  fiabv  42524  prjspner1  42614  0prjspnrel  42615  jm2.26a  42989  onov0suclim  43263  oe0suclim  43266  cantnfresb  43313  onmcl  43320  omcl2  43322  tfsconcatun  43326  naddwordnexlem4  43390  mnringmulrcld  44217  radcnvrat  44303  sumsnd  45020  icccncfext  45885  fperdvper  45917  dvcosax  45924  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  volioc  45970  itgiccshift  45978  stoweidlem34  46032  dirkercncflem2  46102  fourierdlem32  46137  fourierdlem41  46146  fourierdlem48  46152  fourierdlem64  46168  fourierdlem73  46177  fourierdlem79  46183  fourierdlem82  46186  fourierdlem97  46201  fourierdlem101  46205  fourierdlem109  46213  fourierdlem111  46215  fouriersw  46229  elaa2  46232  etransclem24  46256  etransclem25  46257  etransclem46  46278  nnfoctbdjlem  46453  ismeannd  46465  smfpimltxr  46745  smfpimgtxr  46778  ndfatafv2undef  47213  fzopredsuc  47324  m1modmmod  47359  modlt0b  47364  prproropf1olem3  47506  prproropf1olem4  47507  fmtnorec2lem  47543  2pwp1prmfmtno  47591  sfprmdvdsmersenne  47604  sgprmdvdsmersenne  47605  lighneallem2  47607  lighneallem3  47608  dfodd6  47638  dfeven4  47639  m1expevenALTV  47648  isubgredg  47866  upgrimwlklem5  47901  gricushgr  47917  stgrusgra  47958  isubgr3stgrlem8  47972  clintopval  48192  lmod0rng  48217  zlidlring  48222  2zrngagrp  48237  dmmpossx2  48325  zlmodzxzscm  48345  zlmodzxzadd  48346  domnmsuppn0  48357  rmsuppss  48358  scmsuppss  48359  ply1mulgsumlem4  48378  ldepsprlem  48461  lincresunit2  48467  nn0sumshdiglemB  48609  2arymptfv  48639  ackval42  48685  affinecomb1  48691  itschlc0yqe  48749  itsclquadb  48765  2itscp  48770  incat  49590  0setrec  49693