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

Theorem sylan9eqr 2707
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 2705 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 468 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  sbcied2  3506  csbied2  3594  fun2ssres  5969  fcoi1  6116  fcoi2  6117  funssfv  6247  fvtp1  6501  nvof1o  6576  onuninsuci  7082  ot1stg  7224  ot2ndg  7225  el2xptp0  7256  mpt2mptsx  7278  dmmpt2ssx  7280  fmpt2x  7281  2ndconst  7311  mpt2xopoveq  7390  wfrlem10  7469  rdgeq12  7554  rdgsucmptnf  7570  frsucmptn  7579  oev2  7648  oesuclem  7650  oawordeulem  7679  om00  7700  omass  7705  oeoa  7722  oeoe  7724  nnmass  7749  oaabs2  7770  omabs  7772  omxpenlem  8102  sbthlem4  8114  sbthlem6  8116  fodomr  8152  ssenen  8175  fi0  8367  cantnfp1  8616  cnfcomlem  8634  cardaleph  8950  cflim2  9123  axdc4lem  9315  fpwwe2lem12  9501  fpwwe2lem13  9502  rankcf  9637  inatsk  9638  ltrnq  9839  addclprlem1  9876  mulclprlem  9879  1idpr  9889  prlem936  9907  reclem3pr  9909  mulcmpblnrlem  9929  recexsrlem  9962  map2psrpr  9969  addid0  10488  nnnn0addcl  11361  zindd  11516  qaddcl  11842  qmulcl  11844  qreccl  11846  xaddnemnf  12105  xaddnepnf  12106  xaddcom  12109  xnegdi  12116  xaddass  12117  xpncan  12119  xleadd1a  12121  xlt2add  12128  rexmul  12139  xmulgt0  12151  xmulge0  12152  xmulasslem3  12154  xlemul1a  12156  xadddilem  12162  xadddi2  12165  modmuladd  12752  modm1p1mod0  12761  modfzo0difsn  12782  seqf1olem2  12881  expp1  12907  expneg  12908  expcllem  12911  mulexp  12939  expmul  12945  sqoddm1div8  13068  bcpasc  13148  hashrabsn01  13200  fseq1hash  13203  hashinfxadd  13212  hashfzo  13254  fnfz0hash  13268  ffzo0hash  13271  hashf1lem1  13277  hashge2el2dif  13300  brfi1indlem  13316  lsw0  13385  ccatval1  13395  ccatval2  13396  swrdval  13462  reuccats1  13526  splval  13548  repswswrd  13577  2cshwcshw  13617  s4dom  13710  wrdlen2i  13732  shftfn  13857  reim0b  13903  cjexp  13934  sqeqd  13950  fsumser  14505  sumsnf  14517  sumsn  14519  binomlem  14605  expcnv  14640  prodsn  14736  prodsnf  14738  bpolylem  14823  bpoly2  14832  bpoly3  14833  ef0lem  14853  dvdsnegb  15046  mod2eq1n2dvds  15118  m1expe  15138  m1expo  15139  m1exp1  15140  flodddiv4  15184  sadadd2lem2  15219  gcdabs  15297  bezoutr1  15329  dvdslcm  15358  lcmeq0  15360  lcmcl  15361  lcmabs  15365  lcmgcdlem  15366  lcmdvds  15368  lcmf0val  15382  lcmftp  15396  lcmfunsnlem2  15400  coprmdvdsOLD  15414  mulgcddvds  15416  divgcdcoprmex  15427  pcge0  15613  pcadd  15640  pcmpt2  15644  prmreclem4  15670  ramval  15759  ramcl  15780  fvprmselelfz  15795  fvprmselgcd1  15796  ressid2  15975  ressval2  15976  mrcmndind  17413  frmdval  17435  mgm2nsgrplem3  17454  mulgfval  17589  mulgnn0subcl  17601  mulgnn0z  17614  isga  17770  symgval  17845  symgextfve  17885  symgfixf1  17903  f1omvdco2  17914  psgnsn  17986  odid  18003  gexid  18042  frgpuptinv  18230  frgpup2  18235  dprdsn  18481  srgmulgass  18577  srgpcomp  18578  srgbinomlem4  18589  ringinvnzdiv  18639  f1rhm0to0  18788  f1rhm0to0ALT  18789  isabvd  18868  issrng  18898  lmodvsmmulgdi  18946  mptscmfsupp0  18976  lvecinv  19161  lspdisj2  19175  lspfixed  19176  lspexch  19177  sralem  19225  srasca  19229  sravsca  19230  sraip  19231  assamulgscmlem2  19397  mplval  19476  opsrval  19522  cply1mul  19712  gsummoncoe1  19722  evl1fval  19740  znval  19931  psgndiflemB  19994  isphl  20021  scmate  20364  scmatscm  20367  mdetdiagid  20454  mdetunilem7  20472  mdetuni0  20475  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  slesolinvbi  20535  cpmatacl  20569  cpmatinvcl  20570  pmatcollpw2lem  20630  monmatcollpw  20632  pmatcollpwfi  20635  mp2pm2mplem4  20662  pm2mp  20678  cpmadugsumlemF  20729  cpmadugsumfi  20730  cpmadumatpoly  20736  cayhamlem4  20741  cayleyhamilton0  20742  cayleyhamiltonALT  20744  indistopon  20853  0ntr  20923  pnrmopn  21195  reftr  21365  kgenval  21386  pt1hmeo  21657  fmval  21794  fmf  21796  istmd  21925  istgp  21928  tsmsval2  21980  isxmet2d  22179  xpsxmetlem  22231  xpsmet  22234  blfvalps  22235  tmsval  22333  isnlm  22526  nmoleub  22582  idnghm  22594  blssioo  22645  blcvx  22648  icccvx  22796  pcorevlem  22872  isclm  22910  caufval  23119  iscms  23188  mbfsup  23476  i1f1  23502  dvexp3  23786  rolle  23798  dvivth  23818  deg1add  23908  0dgr  24046  coefv0  24049  elqaalem2  24120  dvradcnv  24220  abelthlem8  24238  efper  24276  logtayl  24451  abscxpbnd  24539  relogbcxpb  24570  dcubic2  24616  rlimcnp2  24738  cvxcl  24756  zetacvg  24786  lgamgulmlem2  24801  vmaval  24884  chtub  24982  logexprlim  24995  dchrsum2  25038  sumdchr2  25040  bposlem2  25055  lgsdir  25102  lgsne0  25105  lgsdirnn0  25114  lgsdinn0  25115  lgsquadlem2  25151  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  dchrvmasum2if  25231  dchrvmasumiflem1  25235  rpvmasum2  25246  pntpbnd1  25320  ostth2lem4  25370  trgcgrg  25455  ax5seglem1  25853  ax5seglem2  25854  ax5seglem5  25858  usgr1vr  26192  cplgr2vpr  26385  cplgr3v  26387  cusgrrusgr  26533  wlklenvm1  26573  wlk0prc  26606  wlksoneq1eq2  26616  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem6  26763  crctcshlem4  26768  crctcsh  26772  wlkiswwlks1  26821  wwlksnextbi  26857  wwlksnextwrd  26860  midwwlks2s3  26917  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2a4  26963  clwlkclwwlklem3  26967  clwwisshclwws  26972  erclwwlkeqlen  26976  clwwlkinwwlk  27003  clwwlkn2  27007  clwwlkf  27010  clwwlkf1  27012  wwlksext2clwwlkOLD  27022  eleclclwwlknlem2  27026  erclwwlkneqlen  27032  umgrhashecclwwlk  27042  eucrctshift  27221  eucrct2eupth  27223  fusgr2wsp2nb  27314  grpoidinvlem2  27487  vcz  27558  nvz  27652  lnon0  27781  ipasslem2  27815  htthlem  27902  hvpncan  28024  hiidge0  28083  normgt0  28112  hsn0elch  28233  shsel3  28302  spansneleq  28557  normcan  28563  h1datomi  28568  fh1  28605  spansncvi  28639  5oalem1  28641  5oalem3  28643  5oalem5  28645  3oalem2  28650  pjdsi  28699  kbpj  28943  0hmop  28970  0lnfn  28972  adj0  28981  nlelshi  29047  branmfn  29092  opsqrlem1  29127  hst1h  29214  mdsl0  29297  superpos  29341  sumdmdlem  29405  cdj3lem1  29421  f1od2  29627  xrpxdivcld  29771  2sqn0  29774  xrge0npcan  29822  resvid2  29956  resvval2  29957  esumsnf  30254  esummulc1  30271  measxun2  30401  omsmeas  30513  sibfof  30530  probun  30609  bnj517  31081  mrsubfval  31531  msrval  31561  subdivcomb2  31738  dfrdg2  31825  bj-bary1lem1  33291  rdgeqoa  33348  finxpreclem2  33357  finxpreclem3  33360  matunitlindflem1  33535  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem14  33553  poimirlem15  33554  poimirlem17  33556  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  mblfinlem2  33577  mblfinlem3  33578  ismblfin  33580  mbfposadd  33587  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  ftc1anclem8  33622  areacirc  33635  ismtyval  33729  ismrer1  33767  grposnOLD  33811  rabeq12f  34095  csbeq12  34096  iuneq12f  34102  lsatcv1  34653  glbconN  34981  atltcvr  35039  3dim2  35072  islln2a  35121  2at0mat0  35129  islpln2a  35152  islvol2aN  35196  pmodlem2  35451  pmapjat1  35457  pcl0bN  35527  osumclN  35571  pexmidALTN  35582  lhp2at0nle  35639  4atexlemunv  35670  cdleme18b  35897  cdleme31sn1  35986  cdleme31sde  35990  cdleme31sn2  35994  ltrniotavalbN  36189  trljco  36345  cdlemh  36422  cdlemk40t  36523  cdlemk40f  36524  cdleml9  36589  dihmeetlem3N  36911  dochkrshp  36992  dihprrn  37032  dihjat1  37035  dvh3dim  37052  dochkrsm  37064  dochexmid  37074  lcfl7lem  37105  lcfl9a  37111  lclkrlem1  37112  mapdspex  37274  mapdindp2  37327  mapdh6dN  37345  hdmap1l6d  37420  hdmap11lem2  37451  hdmap14lem4a  37480  hdmapip0  37524  hlhilset  37543  jm2.26a  37884  radcnvrat  38830  sumsnd  39499  icccncfext  40418  fperdvper  40451  dvcosax  40459  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  volioc  40506  itgiccshift  40514  stoweidlem34  40569  dirkercncflem2  40639  fourierdlem32  40674  fourierdlem41  40683  fourierdlem48  40689  fourierdlem64  40705  fourierdlem73  40714  fourierdlem79  40720  fourierdlem82  40723  fourierdlem97  40738  fourierdlem101  40742  fourierdlem109  40750  fourierdlem111  40752  fouriersw  40766  elaa2  40769  etransclem24  40793  etransclem25  40794  etransclem46  40815  nnfoctbdjlem  40990  ismeannd  41002  fzopredsuc  41658  fmtnorec2lem  41779  2pwp1prmfmtno  41829  sfprmdvdsmersenne  41845  sgprmdvdsmersenne  41846  lighneallem2  41848  lighneallem3  41849  dfodd6  41875  dfeven4  41876  m1expevenALTV  41885  clintopval  42165  lmod0rng  42193  2zrngagrp  42268  rngcval  42287  ringcval  42333  dmmpt2ssx2  42440  zlmodzxzscm  42460  zlmodzxzadd  42461  domnmsuppn0  42475  rmsuppss  42476  scmsuppss  42478  ply1mulgsumlem4  42502  ldepsprlem  42586  lincresunit2  42592  m1modmmod  42641  nn0sumshdiglemB  42739  0setrec  42775
  Copyright terms: Public domain W3C validator