Theorem sylan9eqr 2792

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  sbcied2  3823  csbied2  3932  opthhausdorff0  5517  fun2ssres  6592  fcoi1  6764  fcoi2  6765  funssfv  6911  fvtp1  7197  nvof1o  7280  onuninsuci  7831  ot1stg  7991  ot2ndg  7992  el2xptp0  8024  mpomptsx  8052  dmmpossx  8054  fmpox  8055  2ndconst  8089  offsplitfpar  8107  mpoxopoveq  8206  wfrlem10OLD  8320  rdgeq12  8415  rdgsucmptnf  8431  frsucmptn  8441  oev2  8525  oesuclem  8527  oawordeulem  8556  om00  8577  omass  8582  omeulem1  8584  oeoa  8599  oeoe  8601  nnmass  8626  oaabs2  8650  omabs  8652  mapsnend  9038  omxpenlem  9075  sbthlem4  9088  sbthlem6  9090  fodomr  9130  ssenen  9153  fi0  9417  cantnfp1  9678  cnfcomlem  9696  ttrclselem2  9723  cardaleph  10086  cflim2  10260  axdc4lem  10452  fpwwe2lem11  10638  fpwwe2lem12  10639  rankcf  10774  inatsk  10775  ltrnq  10976  addclprlem1  11013  mulclprlem  11016  1idpr  11026  prlem936  11044  reclem3pr  11046  mulcmpblnrlem  11067  recexsrlem  11100  map2psrpr  11107  addid0  11637  subdivcomb2  11914  nnnn0addcl  12506  zindd  12667  qaddcl  12953  qmulcl  12955  qreccl  12957  xaddnemnf  13219  xaddnepnf  13220  xaddcom  13223  xnegdi  13231  xaddass  13232  xpncan  13234  xleadd1a  13236  xlt2add  13243  rexmul  13254  xmulgt0  13266  xmulge0  13267  xmulasslem3  13269  xlemul1a  13271  xadddilem  13277  xadddi2  13280  modmuladd  13882  modm1p1mod0  13891  modfzo0difsn  13912  seqf1olem2  14012  expp1  14038  expneg  14039  expcllem  14042  mulexp  14071  expmul  14077  sqoddm1div8  14210  bcpasc  14285  hashrabsn01  14337  fseq1hash  14340  hashinfxadd  14349  hashfzo  14393  fnfz0hash  14409  ffzo0hash  14412  hashf1lem1  14419  hashf1lem1OLD  14420  hashge2el2dif  14445  hashdifsnp1  14461  lsw0  14519  ccatval1  14531  ccatval2  14532  swrdval  14597  ccatopth  14670  reuccatpfxs1  14701  splval  14705  repswswrd  14738  2cshwcshw  14780  s4dom  14874  wrdlen2i  14897  shftfn  15024  reim0b  15070  cjexp  15101  sqeqd  15117  fsumser  15680  sumsnf  15693  binomlem  15779  expcnv  15814  prodsn  15910  prodsnf  15912  bpolylem  15996  bpoly2  16005  bpoly3  16006  ef0lem  16026  dvdsnegb  16221  mod2eq1n2dvds  16294  m1expe  16321  m1expo  16322  m1exp1  16323  flodddiv4  16360  sadadd2lem2  16395  gcdabsOLD  16477  bezoutr1  16510  dvdslcm  16539  lcmeq0  16541  lcmcl  16542  lcmabs  16546  lcmgcdlem  16547  lcmdvds  16549  lcmf0val  16563  lcmftp  16577  lcmfunsnlem2  16581  mulgcddvds  16596  divgcdcoprmex  16607  pcge0  16799  pcadd  16826  pcmpt2  16830  prmreclem4  16856  ramval  16945  ramcl  16966  fvprmselelfz  16981  fvprmselgcd1  16982  ressid2  17181  ressval2  17182  mndind  18745  frmdval  18768  efmnd  18787  smndex1igid  18821  smndex1n0mnd  18829  mgm2nsgrplem3  18837  mulgfval  18988  mulgfvalALT  18989  mulgnn0subcl  19003  mulgnn0z  19017  cycsubm  19117  f1ghm0to0  19159  isga  19196  symgextfve  19328  symgfixf1  19346  f1omvdco2  19357  psgnsn  19429  odid  19447  gexid  19490  efgsval2  19642  frgpuptinv  19680  frgpup2  19685  dprdsn  19947  srgmulgass  20111  srgpcomp  20112  srgbinomlem4  20123  ringinvnzdiv  20189  isabvd  20571  issrng  20601  lmodvsmmulgdi  20651  mptscmfsupp0  20681  lvecinv  20871  lspdisj2  20885  lspfixed  20886  lspexch  20887  sralem  20935  sralemOLD  20936  srasca  20943  srascaOLD  20944  sravsca  20945  sravscaOLD  20946  sraip  20947  znval  21306  psgndiflemB  21372  isphl  21400  assamulgscmlem2  21673  mplval  21767  opsrval  21820  cply1mul  22038  gsummoncoe1  22048  evl1fval  22067  scmate  22232  scmatscm  22235  mdetdiagid  22322  mdetunilem7  22340  mdetuni0  22343  gsummatr01lem3  22379  gsummatr01lem4  22380  gsummatr01  22381  slesolinvbi  22403  cpmatacl  22438  cpmatinvcl  22439  pmatcollpw2lem  22499  monmatcollpw  22501  pmatcollpwfi  22504  mp2pm2mplem4  22531  pm2mp  22547  cpmadugsumlemF  22598  cpmadugsumfi  22599  cpmadumatpoly  22605  cayhamlem4  22610  cayleyhamilton0  22611  cayleyhamiltonALT  22613  indistopon  22724  0ntr  22795  pnrmopn  23067  reftr  23238  kgenval  23259  pt1hmeo  23530  fmval  23667  fmf  23669  istmd  23798  istgp  23801  tsmsval2  23854  isxmet2d  24053  xpsxmetlem  24105  xpsmet  24108  blfvalps  24109  tmsval  24209  isnlm  24412  nmoleub  24468  idnghm  24480  blssioo  24531  blcvx  24534  icccvx  24695  pcorevlem  24773  isclm  24811  caufval  25023  iscms  25093  mbfsup  25413  i1f1  25439  dvexp3  25730  rolle  25742  dvivth  25762  deg1add  25856  0dgr  25994  coefv0  25997  elqaalem2  26069  dvradcnv  26169  abelthlem8  26187  efper  26225  logtayl  26404  abscxpbnd  26497  relogbcxpb  26528  logbgcd1irr  26535  dcubic2  26585  rlimcnp2  26707  cvxcl  26725  zetacvg  26755  lgamgulmlem2  26770  vmaval  26853  chtub  26951  logexprlim  26964  dchrsum2  27007  sumdchr2  27009  bposlem2  27024  lgsdir  27071  lgsne0  27074  lgsdirnn0  27083  lgsdinn0  27084  lgsquadlem2  27120  2lgslem3a  27135  2lgslem3b  27136  2lgslem3c  27137  2lgslem3d  27138  2lgslem3a1  27139  2lgslem3b1  27140  2lgslem3c1  27141  2lgslem3d1  27142  2sqn0  27173  dchrvmasum2if  27236  dchrvmasumiflem1  27240  rpvmasum2  27251  pntpbnd1  27325  ostth2lem4  27375  trgcgrg  28033  tgcgr4  28049  ax5seglem1  28453  ax5seglem2  28454  ax5seglem5  28458  usgr1vr  28779  cplgr2vpr  28957  cplgr3v  28959  cusgrrusgr  29105  wlklenvm1  29146  wlk0prc  29178  wlksoneq1eq2  29188  crctcshwlkn0lem4  29334  crctcshwlkn0lem5  29335  crctcshwlkn0lem6  29336  crctcshlem4  29341  crctcsh  29345  wlkiswwlks1  29388  wwlksnext  29414  wwlksnextbi  29415  wwlksnextwrd  29418  midwwlks2s3  29473  clwlkclwwlklem2fv1  29515  clwlkclwwlklem2a4  29517  clwlkclwwlklem3  29521  clwwisshclwws  29535  erclwwlkeqlen  29539  clwwlkinwwlk  29560  clwwlkn2  29564  clwwlkf  29567  clwwlkf1  29569  eleclclwwlknlem2  29581  erclwwlkneqlen  29588  umgrhashecclwwlk  29598  eucrctshift  29763  eucrct2eupth  29765  fusgr2wsp2nb  29854  grpoidinvlem2  30025  vcz  30095  nvz  30189  lnon0  30318  ipasslem2  30352  htthlem  30437  hvpncan  30559  hiidge0  30618  normgt0  30647  hsn0elch  30768  shsel3  30835  spansneleq  31090  normcan  31096  h1datomi  31101  fh1  31138  spansncvi  31172  5oalem1  31174  5oalem3  31176  5oalem5  31178  3oalem2  31183  pjdsi  31232  kbpj  31476  0hmop  31503  0lnfn  31505  adj0  31514  nlelshi  31580  branmfn  31625  opsqrlem1  31660  hst1h  31747  mdsl0  31830  superpos  31874  sumdmdlem  31938  cdj3lem1  31954  f1od2  32213  xrpxdivcld  32368  xrge0npcan  32462  resvid2  32712  resvval2  32713  qsdrng  32885  r1pquslmic  32956  esumsnf  33360  esummulc1  33377  measxun2  33506  omsmeas  33620  sibfof  33637  probun  33716  signstfvn  33878  bnj517  34194  pthhashvtx  34416  ex-sategoelel  34710  mrsubfval  34797  msrval  34827  dfrdg2  35071  bj-prmoore  36299  bj-bary1lem1  36495  rdgeqoa  36554  finxpreclem2  36574  finxpreclem3  36577  matunitlindflem1  36787  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem14  36805  poimirlem15  36806  poimirlem17  36808  poimirlem20  36811  poimirlem22  36813  poimirlem23  36814  poimirlem24  36815  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  mblfinlem2  36829  mblfinlem3  36830  ismblfin  36832  mbfposadd  36838  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  ftc1anclem8  36871  areacirc  36884  ismtyval  36971  ismrer1  37009  grposnOLD  37053  rabeq12f  37328  csbeq12  37329  iuneq12f  37334  lsatcv1  38221  glbconN  38550  glbconNOLD  38551  atltcvr  38609  3dim2  38642  islln2a  38691  2at0mat0  38699  islpln2a  38722  islvol2aN  38766  pmodlem2  39021  pmapjat1  39027  pcl0bN  39097  osumclN  39141  pexmidALTN  39152  lhp2at0nle  39209  4atexlemunv  39240  cdleme18b  39466  cdleme31sn1  39555  cdleme31sde  39559  cdleme31sn2  39563  ltrniotavalbN  39758  trljco  39914  cdlemh  39991  cdlemk40t  40092  cdlemk40f  40093  cdleml9  40158  dihmeetlem3N  40479  dochkrshp  40560  dihprrn  40600  dihjat1  40603  dvh3dim  40620  dochkrsm  40632  dochexmid  40642  lcfl7lem  40673  lcfl9a  40679  lclkrlem1  40680  mapdspex  40842  mapdindp2  40895  mapdh6dN  40913  hdmap1l6d  40987  hdmap11lem2  41016  hdmap14lem4a  41045  hdmapip0  41089  hlhilset  41108  nnadd1com  41483  sn-negex12  41591  prjspner1  41670  0prjspnrel  41671  jm2.26a  42041  onov0suclim  42326  oe0suclim  42329  cantnfresb  42376  onmcl  42383  omcl2  42385  tfsconcatun  42389  naddwordnexlem4  42454  mnringmulrcld  43289  radcnvrat  43375  sumsnd  44012  icccncfext  44901  fperdvper  44933  dvcosax  44940  ioodvbdlimc1lem1  44945  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  volioc  44986  itgiccshift  44994  stoweidlem34  45048  dirkercncflem2  45118  fourierdlem32  45153  fourierdlem41  45162  fourierdlem48  45168  fourierdlem64  45184  fourierdlem73  45193  fourierdlem79  45199  fourierdlem82  45202  fourierdlem97  45217  fourierdlem101  45221  fourierdlem109  45229  fourierdlem111  45231  fouriersw  45245  elaa2  45248  etransclem24  45272  etransclem25  45273  etransclem46  45294  nnfoctbdjlem  45469  ismeannd  45481  smfpimltxr  45761  smfpimgtxr  45794  ndfatafv2undef  46218  fzopredsuc  46329  prproropf1olem3  46471  prproropf1olem4  46472  fmtnorec2lem  46508  2pwp1prmfmtno  46556  sfprmdvdsmersenne  46569  sgprmdvdsmersenne  46570  lighneallem2  46572  lighneallem3  46573  dfodd6  46603  dfeven4  46604  m1expevenALTV  46613  isomushgr  46792  isomuspgrlem2d  46797  clintopval  46880  lmod0rng  46908  zlidlring  46914  2zrngagrp  46929  rngcval  46948  ringcval  46994  dmmpossx2  47100  zlmodzxzscm  47121  zlmodzxzadd  47122  domnmsuppn0  47133  rmsuppss  47134  scmsuppss  47136  ply1mulgsumlem4  47157  ldepsprlem  47240  lincresunit2  47246  m1modmmod  47294  nn0sumshdiglemB  47393  2arymptfv  47423  ackval42  47469  affinecomb1  47475  itschlc0yqe  47533  itsclquadb  47549  2itscp  47554  0setrec  47836