MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9eqr Structured version   Visualization version   GIF version

Theorem sylan9eqr 2858
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
StepHypRef Expression
1 sylan9eqr.1 . . 3 (𝜑𝐴 = 𝐵)
2 sylan9eqr.2 . . 3 (𝜓𝐵 = 𝐶)
31, 2sylan9eq 2856 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 462 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538
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 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794
This theorem is referenced by:  sbcied2  3766  csbied2  3868  opthhausdorff0  5376  fun2ssres  6373  fcoi1  6530  fcoi2  6531  funssfv  6670  fvtp1  6938  nvof1o  7019  onuninsuci  7539  ot1stg  7689  ot2ndg  7690  el2xptp0  7722  mpomptsx  7748  dmmpossx  7750  fmpox  7751  2ndconst  7783  offsplitfpar  7802  mpoxopoveq  7872  wfrlem10  7951  rdgeq12  8036  rdgsucmptnf  8052  frsucmptn  8061  oev2  8135  oesuclem  8137  oawordeulem  8167  om00  8188  omass  8193  omeulem1  8195  oeoa  8210  oeoe  8212  nnmass  8237  oaabs2  8259  omabs  8261  mapsnend  8575  omxpenlem  8605  sbthlem4  8618  sbthlem6  8620  fodomr  8656  ssenen  8679  fi0  8872  cantnfp1  9132  cnfcomlem  9150  cardaleph  9504  cflim2  9678  axdc4lem  9870  fpwwe2lem12  10056  fpwwe2lem13  10057  rankcf  10192  inatsk  10193  ltrnq  10394  addclprlem1  10431  mulclprlem  10434  1idpr  10444  prlem936  10462  reclem3pr  10464  mulcmpblnrlem  10485  recexsrlem  10518  map2psrpr  10525  addid0  11052  subdivcomb2  11329  nnnn0addcl  11919  zindd  12075  qaddcl  12356  qmulcl  12358  qreccl  12360  xaddnemnf  12621  xaddnepnf  12622  xaddcom  12625  xnegdi  12633  xaddass  12634  xpncan  12636  xleadd1a  12638  xlt2add  12645  rexmul  12656  xmulgt0  12668  xmulge0  12669  xmulasslem3  12671  xlemul1a  12673  xadddilem  12679  xadddi2  12682  modmuladd  13280  modm1p1mod0  13289  modfzo0difsn  13310  seqf1olem2  13410  expp1  13436  expneg  13437  expcllem  13440  mulexp  13468  expmul  13474  sqoddm1div8  13604  bcpasc  13681  hashrabsn01  13734  fseq1hash  13737  hashinfxadd  13746  hashfzo  13790  fnfz0hash  13804  ffzo0hash  13807  hashf1lem1  13813  hashge2el2dif  13838  hashdifsnp1  13854  lsw0  13912  ccatval1  13925  ccatval1OLD  13926  ccatval2  13927  swrdval  14000  ccatopth  14073  reuccatpfxs1  14104  splval  14108  repswswrd  14141  2cshwcshw  14182  s4dom  14276  wrdlen2i  14299  shftfn  14427  reim0b  14473  cjexp  14504  sqeqd  14520  fsumser  15082  sumsnf  15094  binomlem  15179  expcnv  15214  prodsn  15311  prodsnf  15313  bpolylem  15397  bpoly2  15406  bpoly3  15407  ef0lem  15427  dvdsnegb  15622  mod2eq1n2dvds  15691  m1expe  15718  m1expo  15719  m1exp1  15720  flodddiv4  15757  sadadd2lem2  15792  gcdabs  15870  bezoutr1  15906  dvdslcm  15935  lcmeq0  15937  lcmcl  15938  lcmabs  15942  lcmgcdlem  15943  lcmdvds  15945  lcmf0val  15959  lcmftp  15973  lcmfunsnlem2  15977  mulgcddvds  15992  divgcdcoprmex  16003  pcge0  16191  pcadd  16218  pcmpt2  16222  prmreclem4  16248  ramval  16337  ramcl  16358  fvprmselelfz  16373  fvprmselgcd1  16374  ressid2  16547  ressval2  16548  mndind  17987  frmdval  18011  efmnd  18030  smndex1igid  18064  smndex1n0mnd  18072  mgm2nsgrplem3  18080  mulgfval  18221  mulgfvalALT  18222  mulgnn0subcl  18236  mulgnn0z  18249  cycsubm  18340  isga  18416  symgextfve  18542  symgfixf1  18560  f1omvdco2  18571  psgnsn  18643  odid  18661  gexid  18701  efgsval2  18854  frgpuptinv  18892  frgpup2  18897  dprdsn  19154  srgmulgass  19277  srgpcomp  19278  srgbinomlem4  19289  ringinvnzdiv  19342  f1ghm0to0  19491  f1rhm0to0ALT  19492  isabvd  19587  issrng  19617  lmodvsmmulgdi  19665  mptscmfsupp0  19695  lvecinv  19881  lspdisj2  19895  lspfixed  19896  lspexch  19897  sralem  19945  srasca  19949  sravsca  19950  sraip  19951  znval  20230  psgndiflemB  20292  isphl  20320  assamulgscmlem2  20589  mplval  20669  opsrval  20717  cply1mul  20926  gsummoncoe1  20936  evl1fval  20955  scmate  21118  scmatscm  21121  mdetdiagid  21208  mdetunilem7  21226  mdetuni0  21229  gsummatr01lem3  21265  gsummatr01lem4  21266  gsummatr01  21267  slesolinvbi  21289  cpmatacl  21324  cpmatinvcl  21325  pmatcollpw2lem  21385  monmatcollpw  21387  pmatcollpwfi  21390  mp2pm2mplem4  21417  pm2mp  21433  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmadumatpoly  21491  cayhamlem4  21496  cayleyhamilton0  21497  cayleyhamiltonALT  21499  indistopon  21609  0ntr  21679  pnrmopn  21951  reftr  22122  kgenval  22143  pt1hmeo  22414  fmval  22551  fmf  22553  istmd  22682  istgp  22685  tsmsval2  22738  isxmet2d  22937  xpsxmetlem  22989  xpsmet  22992  blfvalps  22993  tmsval  23091  isnlm  23284  nmoleub  23340  idnghm  23352  blssioo  23403  blcvx  23406  icccvx  23558  pcorevlem  23634  isclm  23672  caufval  23882  iscms  23952  mbfsup  24271  i1f1  24297  dvexp3  24584  rolle  24596  dvivth  24616  deg1add  24707  0dgr  24845  coefv0  24848  elqaalem2  24919  dvradcnv  25019  abelthlem8  25037  efper  25075  logtayl  25254  abscxpbnd  25345  relogbcxpb  25376  logbgcd1irr  25383  dcubic2  25433  rlimcnp2  25555  cvxcl  25573  zetacvg  25603  lgamgulmlem2  25618  vmaval  25701  chtub  25799  logexprlim  25812  dchrsum2  25855  sumdchr2  25857  bposlem2  25872  lgsdir  25919  lgsne0  25922  lgsdirnn0  25931  lgsdinn0  25932  lgsquadlem2  25968  2lgslem3a  25983  2lgslem3b  25984  2lgslem3c  25985  2lgslem3d  25986  2lgslem3a1  25987  2lgslem3b1  25988  2lgslem3c1  25989  2lgslem3d1  25990  2sqn0  26021  dchrvmasum2if  26084  dchrvmasumiflem1  26088  rpvmasum2  26099  pntpbnd1  26173  ostth2lem4  26223  trgcgrg  26312  tgcgr4  26328  ax5seglem1  26725  ax5seglem2  26726  ax5seglem5  26730  usgr1vr  27048  cplgr2vpr  27226  cplgr3v  27228  cusgrrusgr  27374  wlklenvm1  27414  wlk0prc  27446  wlksoneq1eq2  27457  crctcshwlkn0lem4  27602  crctcshwlkn0lem5  27603  crctcshwlkn0lem6  27604  crctcshlem4  27609  crctcsh  27613  wlkiswwlks1  27656  wwlksnext  27682  wwlksnextbi  27683  wwlksnextwrd  27686  midwwlks2s3  27741  clwlkclwwlklem2fv1  27783  clwlkclwwlklem2a4  27785  clwlkclwwlklem3  27789  clwwisshclwws  27803  erclwwlkeqlen  27807  clwwlkinwwlk  27828  clwwlkn2  27832  clwwlkf  27835  clwwlkf1  27837  eleclclwwlknlem2  27849  erclwwlkneqlen  27856  umgrhashecclwwlk  27866  eucrctshift  28031  eucrct2eupth  28033  fusgr2wsp2nb  28122  grpoidinvlem2  28291  vcz  28361  nvz  28455  lnon0  28584  ipasslem2  28618  htthlem  28703  hvpncan  28825  hiidge0  28884  normgt0  28913  hsn0elch  29034  shsel3  29101  spansneleq  29356  normcan  29362  h1datomi  29367  fh1  29404  spansncvi  29438  5oalem1  29440  5oalem3  29442  5oalem5  29444  3oalem2  29449  pjdsi  29498  kbpj  29742  0hmop  29769  0lnfn  29771  adj0  29780  nlelshi  29846  branmfn  29891  opsqrlem1  29926  hst1h  30013  mdsl0  30096  superpos  30140  sumdmdlem  30204  cdj3lem1  30220  f1od2  30486  xrpxdivcld  30640  xrge0npcan  30731  resvid2  30955  resvval2  30956  esumsnf  31431  esummulc1  31448  measxun2  31577  omsmeas  31689  sibfof  31706  probun  31785  signstfvn  31947  bnj517  32265  pthhashvtx  32482  ex-sategoelel  32776  mrsubfval  32863  msrval  32893  dfrdg2  33148  bj-prmoore  34525  bj-bary1lem1  34720  rdgeqoa  34782  finxpreclem2  34802  finxpreclem3  34805  matunitlindflem1  35046  poimirlem1  35051  poimirlem2  35052  poimirlem3  35053  poimirlem4  35054  poimirlem5  35055  poimirlem6  35056  poimirlem7  35057  poimirlem10  35060  poimirlem11  35061  poimirlem12  35062  poimirlem14  35064  poimirlem15  35065  poimirlem17  35067  poimirlem20  35070  poimirlem22  35072  poimirlem23  35073  poimirlem24  35074  poimirlem25  35075  poimirlem26  35076  poimirlem27  35077  mblfinlem2  35088  mblfinlem3  35089  ismblfin  35091  mbfposadd  35097  itg2addnclem  35101  itg2addnclem3  35103  itg2addnc  35104  ftc1anclem8  35130  areacirc  35143  ismtyval  35231  ismrer1  35269  grposnOLD  35313  rabeq12f  35588  csbeq12  35589  iuneq12f  35594  lsatcv1  36337  glbconN  36666  atltcvr  36724  3dim2  36757  islln2a  36806  2at0mat0  36814  islpln2a  36837  islvol2aN  36881  pmodlem2  37136  pmapjat1  37142  pcl0bN  37212  osumclN  37256  pexmidALTN  37267  lhp2at0nle  37324  4atexlemunv  37355  cdleme18b  37581  cdleme31sn1  37670  cdleme31sde  37674  cdleme31sn2  37678  ltrniotavalbN  37873  trljco  38029  cdlemh  38106  cdlemk40t  38207  cdlemk40f  38208  cdleml9  38273  dihmeetlem3N  38594  dochkrshp  38675  dihprrn  38715  dihjat1  38718  dvh3dim  38735  dochkrsm  38747  dochexmid  38757  lcfl7lem  38788  lcfl9a  38794  lclkrlem1  38795  mapdspex  38957  mapdindp2  39010  mapdh6dN  39028  hdmap1l6d  39102  hdmap11lem2  39131  hdmap14lem4a  39160  hdmapip0  39204  hlhilset  39223  nnadd1com  39455  sn-negex12  39540  0prjspnrel  39600  jm2.26a  39928  mnringmulrcld  40923  radcnvrat  41005  sumsnd  41642  icccncfext  42516  fperdvper  42548  dvcosax  42555  ioodvbdlimc1lem1  42560  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  volioc  42601  itgiccshift  42609  stoweidlem34  42663  dirkercncflem2  42733  fourierdlem32  42768  fourierdlem41  42777  fourierdlem48  42783  fourierdlem64  42799  fourierdlem73  42808  fourierdlem79  42814  fourierdlem82  42817  fourierdlem97  42832  fourierdlem101  42836  fourierdlem109  42844  fourierdlem111  42846  fouriersw  42860  elaa2  42863  etransclem24  42887  etransclem25  42888  etransclem46  42909  nnfoctbdjlem  43081  ismeannd  43093  ndfatafv2undef  43755  fzopredsuc  43867  prproropf1olem3  44009  prproropf1olem4  44010  fmtnorec2lem  44046  2pwp1prmfmtno  44094  sfprmdvdsmersenne  44108  sgprmdvdsmersenne  44109  lighneallem2  44111  lighneallem3  44112  dfodd6  44142  dfeven4  44143  m1expevenALTV  44152  isomushgr  44331  isomuspgrlem2d  44336  clintopval  44451  lmod0rng  44479  zlidlring  44539  2zrngagrp  44554  rngcval  44573  ringcval  44619  dmmpossx2  44725  zlmodzxzscm  44746  zlmodzxzadd  44747  domnmsuppn0  44758  rmsuppss  44759  scmsuppss  44761  ply1mulgsumlem4  44784  ldepsprlem  44868  lincresunit2  44874  m1modmmod  44922  nn0sumshdiglemB  45021  2arymptfv  45051  ackval42  45097  affinecomb1  45103  itschlc0yqe  45161  itsclquadb  45177  2itscp  45182  0setrec  45220
  Copyright terms: Public domain W3C validator