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

Theorem sylan9eqr 2799
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 2797 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 460 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729
This theorem is referenced by:  sbcied2  3791  csbied2  3900  opthhausdorff0  5480  fun2ssres  6551  fcoi1  6721  fcoi2  6722  funssfv  6868  fvtp1  7149  nvof1o  7231  onuninsuci  7781  ot1stg  7940  ot2ndg  7941  el2xptp0  7973  mpomptsx  8001  dmmpossx  8003  fmpox  8004  2ndconst  8038  offsplitfpar  8056  mpoxopoveq  8155  wfrlem10OLD  8269  rdgeq12  8364  rdgsucmptnf  8380  frsucmptn  8390  oev2  8474  oesuclem  8476  oawordeulem  8506  om00  8527  omass  8532  omeulem1  8534  oeoa  8549  oeoe  8551  nnmass  8576  oaabs2  8600  omabs  8602  mapsnend  8987  omxpenlem  9024  sbthlem4  9037  sbthlem6  9039  fodomr  9079  ssenen  9102  fi0  9363  cantnfp1  9624  cnfcomlem  9642  ttrclselem2  9669  cardaleph  10032  cflim2  10206  axdc4lem  10398  fpwwe2lem11  10584  fpwwe2lem12  10585  rankcf  10720  inatsk  10721  ltrnq  10922  addclprlem1  10959  mulclprlem  10962  1idpr  10972  prlem936  10990  reclem3pr  10992  mulcmpblnrlem  11013  recexsrlem  11046  map2psrpr  11053  addid0  11581  subdivcomb2  11858  nnnn0addcl  12450  zindd  12611  qaddcl  12897  qmulcl  12899  qreccl  12901  xaddnemnf  13162  xaddnepnf  13163  xaddcom  13166  xnegdi  13174  xaddass  13175  xpncan  13177  xleadd1a  13179  xlt2add  13186  rexmul  13197  xmulgt0  13209  xmulge0  13210  xmulasslem3  13212  xlemul1a  13214  xadddilem  13220  xadddi2  13223  modmuladd  13825  modm1p1mod0  13834  modfzo0difsn  13855  seqf1olem2  13955  expp1  13981  expneg  13982  expcllem  13985  mulexp  14014  expmul  14020  sqoddm1div8  14153  bcpasc  14228  hashrabsn01  14280  fseq1hash  14283  hashinfxadd  14292  hashfzo  14336  fnfz0hash  14350  ffzo0hash  14353  hashf1lem1  14360  hashf1lem1OLD  14361  hashge2el2dif  14386  hashdifsnp1  14402  lsw0  14460  ccatval1  14472  ccatval2  14473  swrdval  14538  ccatopth  14611  reuccatpfxs1  14642  splval  14646  repswswrd  14679  2cshwcshw  14721  s4dom  14815  wrdlen2i  14838  shftfn  14965  reim0b  15011  cjexp  15042  sqeqd  15058  fsumser  15622  sumsnf  15635  binomlem  15721  expcnv  15756  prodsn  15852  prodsnf  15854  bpolylem  15938  bpoly2  15947  bpoly3  15948  ef0lem  15968  dvdsnegb  16163  mod2eq1n2dvds  16236  m1expe  16263  m1expo  16264  m1exp1  16265  flodddiv4  16302  sadadd2lem2  16337  gcdabsOLD  16419  bezoutr1  16452  dvdslcm  16481  lcmeq0  16483  lcmcl  16484  lcmabs  16488  lcmgcdlem  16489  lcmdvds  16491  lcmf0val  16505  lcmftp  16519  lcmfunsnlem2  16523  mulgcddvds  16538  divgcdcoprmex  16549  pcge0  16741  pcadd  16768  pcmpt2  16772  prmreclem4  16798  ramval  16887  ramcl  16908  fvprmselelfz  16923  fvprmselgcd1  16924  ressid2  17123  ressval2  17124  mndind  18645  frmdval  18668  efmnd  18687  smndex1igid  18721  smndex1n0mnd  18729  mgm2nsgrplem3  18737  mulgfval  18881  mulgfvalALT  18882  mulgnn0subcl  18896  mulgnn0z  18910  cycsubm  19002  isga  19078  symgextfve  19208  symgfixf1  19226  f1omvdco2  19237  psgnsn  19309  odid  19327  gexid  19370  efgsval2  19522  frgpuptinv  19560  frgpup2  19565  dprdsn  19822  srgmulgass  19955  srgpcomp  19956  srgbinomlem4  19967  ringinvnzdiv  20024  f1ghm0to0  20183  f1rhm0to0ALT  20184  isabvd  20295  issrng  20325  lmodvsmmulgdi  20373  mptscmfsupp0  20403  lvecinv  20590  lspdisj2  20604  lspfixed  20605  lspexch  20606  sralem  20654  sralemOLD  20655  srasca  20662  srascaOLD  20663  sravsca  20664  sravscaOLD  20665  sraip  20666  znval  20954  psgndiflemB  21020  isphl  21048  assamulgscmlem2  21319  mplval  21413  opsrval  21463  cply1mul  21681  gsummoncoe1  21691  evl1fval  21710  scmate  21875  scmatscm  21878  mdetdiagid  21965  mdetunilem7  21983  mdetuni0  21986  gsummatr01lem3  22022  gsummatr01lem4  22023  gsummatr01  22024  slesolinvbi  22046  cpmatacl  22081  cpmatinvcl  22082  pmatcollpw2lem  22142  monmatcollpw  22144  pmatcollpwfi  22147  mp2pm2mplem4  22174  pm2mp  22190  cpmadugsumlemF  22241  cpmadugsumfi  22242  cpmadumatpoly  22248  cayhamlem4  22253  cayleyhamilton0  22254  cayleyhamiltonALT  22256  indistopon  22367  0ntr  22438  pnrmopn  22710  reftr  22881  kgenval  22902  pt1hmeo  23173  fmval  23310  fmf  23312  istmd  23441  istgp  23444  tsmsval2  23497  isxmet2d  23696  xpsxmetlem  23748  xpsmet  23751  blfvalps  23752  tmsval  23852  isnlm  24055  nmoleub  24111  idnghm  24123  blssioo  24174  blcvx  24177  icccvx  24329  pcorevlem  24405  isclm  24443  caufval  24655  iscms  24725  mbfsup  25044  i1f1  25070  dvexp3  25358  rolle  25370  dvivth  25390  deg1add  25484  0dgr  25622  coefv0  25625  elqaalem2  25696  dvradcnv  25796  abelthlem8  25814  efper  25852  logtayl  26031  abscxpbnd  26122  relogbcxpb  26153  logbgcd1irr  26160  dcubic2  26210  rlimcnp2  26332  cvxcl  26350  zetacvg  26380  lgamgulmlem2  26395  vmaval  26478  chtub  26576  logexprlim  26589  dchrsum2  26632  sumdchr2  26634  bposlem2  26649  lgsdir  26696  lgsne0  26699  lgsdirnn0  26708  lgsdinn0  26709  lgsquadlem2  26745  2lgslem3a  26760  2lgslem3b  26761  2lgslem3c  26762  2lgslem3d  26763  2lgslem3a1  26764  2lgslem3b1  26765  2lgslem3c1  26766  2lgslem3d1  26767  2sqn0  26798  dchrvmasum2if  26861  dchrvmasumiflem1  26865  rpvmasum2  26876  pntpbnd1  26950  ostth2lem4  27000  trgcgrg  27499  tgcgr4  27515  ax5seglem1  27919  ax5seglem2  27920  ax5seglem5  27924  usgr1vr  28245  cplgr2vpr  28423  cplgr3v  28425  cusgrrusgr  28571  wlklenvm1  28612  wlk0prc  28644  wlksoneq1eq2  28654  crctcshwlkn0lem4  28800  crctcshwlkn0lem5  28801  crctcshwlkn0lem6  28802  crctcshlem4  28807  crctcsh  28811  wlkiswwlks1  28854  wwlksnext  28880  wwlksnextbi  28881  wwlksnextwrd  28884  midwwlks2s3  28939  clwlkclwwlklem2fv1  28981  clwlkclwwlklem2a4  28983  clwlkclwwlklem3  28987  clwwisshclwws  29001  erclwwlkeqlen  29005  clwwlkinwwlk  29026  clwwlkn2  29030  clwwlkf  29033  clwwlkf1  29035  eleclclwwlknlem2  29047  erclwwlkneqlen  29054  umgrhashecclwwlk  29064  eucrctshift  29229  eucrct2eupth  29231  fusgr2wsp2nb  29320  grpoidinvlem2  29489  vcz  29559  nvz  29653  lnon0  29782  ipasslem2  29816  htthlem  29901  hvpncan  30023  hiidge0  30082  normgt0  30111  hsn0elch  30232  shsel3  30299  spansneleq  30554  normcan  30560  h1datomi  30565  fh1  30602  spansncvi  30636  5oalem1  30638  5oalem3  30640  5oalem5  30642  3oalem2  30647  pjdsi  30696  kbpj  30940  0hmop  30967  0lnfn  30969  adj0  30978  nlelshi  31044  branmfn  31089  opsqrlem1  31124  hst1h  31211  mdsl0  31294  superpos  31338  sumdmdlem  31402  cdj3lem1  31418  f1od2  31680  xrpxdivcld  31833  xrge0npcan  31927  resvid2  32159  resvval2  32160  esumsnf  32703  esummulc1  32720  measxun2  32849  omsmeas  32963  sibfof  32980  probun  33059  signstfvn  33221  bnj517  33537  pthhashvtx  33761  ex-sategoelel  34055  mrsubfval  34142  msrval  34172  dfrdg2  34409  bj-prmoore  35615  bj-bary1lem1  35811  rdgeqoa  35870  finxpreclem2  35890  finxpreclem3  35893  matunitlindflem1  36103  poimirlem1  36108  poimirlem2  36109  poimirlem3  36110  poimirlem4  36111  poimirlem5  36112  poimirlem6  36113  poimirlem7  36114  poimirlem10  36117  poimirlem11  36118  poimirlem12  36119  poimirlem14  36121  poimirlem15  36122  poimirlem17  36124  poimirlem20  36127  poimirlem22  36129  poimirlem23  36130  poimirlem24  36131  poimirlem25  36132  poimirlem26  36133  poimirlem27  36134  mblfinlem2  36145  mblfinlem3  36146  ismblfin  36148  mbfposadd  36154  itg2addnclem  36158  itg2addnclem3  36160  itg2addnc  36161  ftc1anclem8  36187  areacirc  36200  ismtyval  36288  ismrer1  36326  grposnOLD  36370  rabeq12f  36645  csbeq12  36646  iuneq12f  36651  lsatcv1  37539  glbconN  37868  glbconNOLD  37869  atltcvr  37927  3dim2  37960  islln2a  38009  2at0mat0  38017  islpln2a  38040  islvol2aN  38084  pmodlem2  38339  pmapjat1  38345  pcl0bN  38415  osumclN  38459  pexmidALTN  38470  lhp2at0nle  38527  4atexlemunv  38558  cdleme18b  38784  cdleme31sn1  38873  cdleme31sde  38877  cdleme31sn2  38881  ltrniotavalbN  39076  trljco  39232  cdlemh  39309  cdlemk40t  39410  cdlemk40f  39411  cdleml9  39476  dihmeetlem3N  39797  dochkrshp  39878  dihprrn  39918  dihjat1  39921  dvh3dim  39938  dochkrsm  39950  dochexmid  39960  lcfl7lem  39991  lcfl9a  39997  lclkrlem1  39998  mapdspex  40160  mapdindp2  40213  mapdh6dN  40231  hdmap1l6d  40305  hdmap11lem2  40334  hdmap14lem4a  40363  hdmapip0  40407  hlhilset  40426  nnadd1com  40812  sn-negex12  40914  prjspner1  40993  0prjspnrel  40994  jm2.26a  41353  onov0suclim  41638  oe0suclim  41641  cantnfresb  41688  onmcl  41695  omcl2  41697  naddwordnexlem4  41747  mnringmulrcld  42582  radcnvrat  42668  sumsnd  43305  icccncfext  44202  fperdvper  44234  dvcosax  44241  ioodvbdlimc1lem1  44246  ioodvbdlimc1lem2  44247  ioodvbdlimc2lem  44249  volioc  44287  itgiccshift  44295  stoweidlem34  44349  dirkercncflem2  44419  fourierdlem32  44454  fourierdlem41  44463  fourierdlem48  44469  fourierdlem64  44485  fourierdlem73  44494  fourierdlem79  44500  fourierdlem82  44503  fourierdlem97  44518  fourierdlem101  44522  fourierdlem109  44530  fourierdlem111  44532  fouriersw  44546  elaa2  44549  etransclem24  44573  etransclem25  44574  etransclem46  44595  nnfoctbdjlem  44770  ismeannd  44782  smfpimltxr  45062  smfpimgtxr  45095  ndfatafv2undef  45518  fzopredsuc  45629  prproropf1olem3  45771  prproropf1olem4  45772  fmtnorec2lem  45808  2pwp1prmfmtno  45856  sfprmdvdsmersenne  45869  sgprmdvdsmersenne  45870  lighneallem2  45872  lighneallem3  45873  dfodd6  45903  dfeven4  45904  m1expevenALTV  45913  isomushgr  46092  isomuspgrlem2d  46097  clintopval  46212  lmod0rng  46240  zlidlring  46300  2zrngagrp  46315  rngcval  46334  ringcval  46380  dmmpossx2  46486  zlmodzxzscm  46507  zlmodzxzadd  46508  domnmsuppn0  46519  rmsuppss  46520  scmsuppss  46522  ply1mulgsumlem4  46544  ldepsprlem  46627  lincresunit2  46633  m1modmmod  46681  nn0sumshdiglemB  46780  2arymptfv  46810  ackval42  46856  affinecomb1  46862  itschlc0yqe  46920  itsclquadb  46936  2itscp  46941  0setrec  47223
  Copyright terms: Public domain W3C validator