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

Theorem sylan9eqr 2665
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 2663 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 467 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602
This theorem is referenced by:  sbcied2  3439  csbied2  3526  fun2ssres  5831  fcoi1  5976  fcoi2  5977  funssfv  6104  fvtp1  6343  nvof1o  6414  onuninsuci  6909  ot1stg  7050  ot2ndg  7051  el2xptp0  7080  mpt2mptsx  7099  dmmpt2ssx  7101  fmpt2x  7102  2ndconst  7130  mpt2xopoveq  7209  wfrlem10  7288  rdgeq12  7373  rdgsucmptnf  7389  frsucmptn  7398  oev2  7467  oesuclem  7469  oawordeulem  7498  om00  7519  omass  7524  oeoa  7541  oeoe  7543  nnmass  7568  oaabs2  7589  omabs  7591  omxpenlem  7923  sbthlem4  7935  sbthlem6  7937  fodomr  7973  ssenen  7996  fi0  8186  cantnfp1  8438  cnfcomlem  8456  cardaleph  8772  cflim2  8945  axdc4lem  9137  fpwwe2lem12  9319  fpwwe2lem13  9320  rankcf  9455  inatsk  9456  ltrnq  9657  addclprlem1  9694  mulclprlem  9697  1idpr  9707  prlem936  9725  reclem3pr  9727  mulcmpblnrlem  9747  recexsrlem  9780  map2psrpr  9787  addid0  10301  nnnn0addcl  11170  zindd  11310  qaddcl  11636  qmulcl  11638  qreccl  11640  xaddnemnf  11899  xaddnepnf  11900  xaddcom  11903  xnegdi  11907  xaddass  11908  xpncan  11910  xleadd1a  11912  xlt2add  11919  rexmul  11930  xmulgt0  11942  xmulge0  11943  xmulasslem3  11945  xlemul1a  11947  xadddilem  11953  xadddi2  11956  modmuladd  12529  modm1p1mod0  12538  modfzo0difsn  12559  seqf1olem2  12658  expp1  12684  expneg  12685  expcllem  12688  mulexp  12716  expmul  12722  sqoddm1div8  12845  bcpasc  12925  hashrabsn01  12975  fseq1hash  12978  hashinfxadd  12987  hashfzo  13028  fnfz0hash  13039  ffzo0hash  13042  hashf1lem1  13048  hashge2el2dif  13067  brfi1indlem  13079  lsw0  13151  ccatval1  13160  ccatval2  13161  swrdval  13215  reuccats1  13278  splval  13299  repswswrd  13328  2cshwcshw  13368  s4dom  13460  wrdlen2i  13480  shftfn  13607  reim0b  13653  cjexp  13684  sqeqd  13700  fsumser  14254  sumsn  14265  binomlem  14346  expcnv  14381  prodsn  14477  prodsnf  14479  bpolylem  14564  bpoly2  14573  bpoly3  14574  ef0lem  14594  dvdsnegb  14783  mod2eq1n2dvds  14855  m1expe  14875  m1expo  14876  m1exp1  14877  flodddiv4  14921  sadadd2lem2  14956  gcdabs  15034  bezoutr1  15066  dvdslcm  15095  lcmeq0  15097  lcmcl  15098  lcmabs  15102  lcmgcdlem  15103  lcmdvds  15105  lcmf0val  15119  lcmftp  15133  lcmfunsnlem2  15137  coprmdvdsOLD  15151  mulgcddvds  15153  divgcdcoprmex  15164  pcge0  15350  pcadd  15377  pcmpt2  15381  prmreclem4  15407  ramval  15496  ramcl  15517  fvprmselelfz  15532  fvprmselgcd1  15533  ressid2  15701  ressval2  15702  mrcmndind  17135  frmdval  17157  mgm2nsgrplem3  17176  mulgfval  17311  mulgnn0subcl  17323  mulgnn0z  17336  isga  17493  symgval  17568  symgextfve  17608  symgfixf1  17626  f1omvdco2  17637  psgnsn  17709  odid  17726  gexid  17765  frgpuptinv  17953  frgpup2  17958  dprdsn  18204  srgmulgass  18300  srgpcomp  18301  srgbinomlem4  18312  ringinvnzdiv  18362  f1rhm0to0  18509  f1rhm0to0ALT  18510  isabvd  18589  issrng  18619  lmodvsmmulgdi  18667  mptscmfsupp0  18697  lvecinv  18880  lspdisj2  18894  lspfixed  18895  lspexch  18896  sralem  18944  srasca  18948  sravsca  18949  sraip  18950  assamulgscmlem2  19116  mplval  19195  opsrval  19241  cply1mul  19431  gsummoncoe1  19441  evl1fval  19459  znval  19647  psgndiflemB  19710  isphl  19737  scmate  20077  scmatscm  20080  mdetdiagid  20167  mdetunilem7  20185  mdetuni0  20188  gsummatr01lem3  20224  gsummatr01lem4  20225  gsummatr01  20226  slesolinvbi  20248  cpmatacl  20282  cpmatinvcl  20283  pmatcollpw2lem  20343  monmatcollpw  20345  pmatcollpwfi  20348  mp2pm2mplem4  20375  pm2mp  20391  cpmadugsumlemF  20442  cpmadugsumfi  20443  cpmadumatpoly  20449  cayhamlem4  20454  cayleyhamilton0  20455  cayleyhamiltonALT  20457  indistopon  20557  0ntr  20627  pnrmopn  20899  reftr  21069  kgenval  21090  pt1hmeo  21361  fmval  21499  fmf  21501  istmd  21630  istgp  21633  tsmsval2  21685  isxmet2d  21883  xpsxmetlem  21935  xpsmet  21938  blfvalps  21939  tmsval  22037  isnlm  22222  nmoleub  22277  idnghm  22289  blssioo  22338  blcvx  22341  icccvx  22488  pcorevlem  22565  isclm  22603  caufval  22799  iscms  22867  mbfsup  23154  i1f1  23180  dvexp3  23462  rolle  23474  dvivth  23494  deg1add  23584  0dgr  23722  coefv0  23725  elqaalem2  23796  dvradcnv  23896  abelthlem8  23914  efper  23952  logtayl  24123  abscxpbnd  24211  relogbcxpb  24242  dcubic2  24288  rlimcnp2  24410  cvxcl  24428  zetacvg  24458  lgamgulmlem2  24473  vmaval  24556  chtub  24654  logexprlim  24667  dchrsum2  24710  sumdchr2  24712  bposlem2  24727  lgsdir  24774  lgsne0  24777  lgsdirnn0  24786  lgsdinn0  24787  lgsquadlem2  24823  2lgslem3a  24838  2lgslem3b  24839  2lgslem3c  24840  2lgslem3d  24841  2lgslem3a1  24842  2lgslem3b1  24843  2lgslem3c1  24844  2lgslem3d1  24845  dchrvmasum2if  24903  dchrvmasumiflem1  24907  rpvmasum2  24918  pntpbnd1  24992  ostth2lem4  25042  trgcgrg  25128  ax5seglem1  25526  ax5seglem2  25527  ax5seglem5  25531  usgraedgprv  25671  wwlknimp  25981  wwlknextbi  26019  wwlkextwrd  26022  clwlkisclwwlklem2fv1  26076  clwlkisclwwlklem2a4  26078  clwlkisclwwlklem0  26082  clwwlkf  26088  clwwlkf1  26090  wwlkext2clwwlk  26097  clwwisshclww  26101  erclwwlkeqlen  26106  eleclclwwlknlem2  26112  erclwwlkneqlen  26118  usghashecclwwlk  26128  vdgr1d  26196  vdgr1b  26197  vdgr1a  26199  cusgraisrusgra  26231  rusgra0edg  26248  eupatrl  26261  usg2spot2nb  26358  grpoidinvlem2  26509  vcz  26591  nvz  26702  lnon0  26843  ipasslem2  26877  htthlem  26964  hvpncan  27086  hiidge0  27145  normgt0  27174  hsn0elch  27295  shsel3  27364  spansneleq  27619  normcan  27625  h1datomi  27630  fh1  27667  spansncvi  27701  5oalem1  27703  5oalem3  27705  5oalem5  27707  3oalem2  27712  pjdsi  27761  kbpj  28005  0hmop  28032  0lnfn  28034  adj0  28043  nlelshi  28109  branmfn  28154  opsqrlem1  28189  hst1h  28276  mdsl0  28359  superpos  28403  sumdmdlem  28467  cdj3lem1  28483  xrpxdivcld  28780  2sqn0  28783  xrge0npcan  28831  resvid2  28965  resvval2  28966  esumsnf  29259  esummulc1  29276  measxun2  29406  omsmeas  29518  sibfof  29535  probun  29614  bnj517  30015  mrsubfval  30465  msrval  30495  subdivcomb2  30671  dfrdg2  30751  bj-bary1lem1  32134  rdgeqoa  32190  finxpreclem2  32199  finxpreclem3  32202  matunitlindflem1  32371  poimirlem1  32376  poimirlem2  32377  poimirlem3  32378  poimirlem4  32379  poimirlem5  32380  poimirlem6  32381  poimirlem7  32382  poimirlem10  32385  poimirlem11  32386  poimirlem12  32387  poimirlem14  32389  poimirlem15  32390  poimirlem17  32392  poimirlem20  32395  poimirlem22  32397  poimirlem23  32398  poimirlem24  32399  poimirlem25  32400  poimirlem26  32401  poimirlem27  32402  mblfinlem2  32413  mblfinlem3  32414  ismblfin  32416  mbfposadd  32423  itg2addnclem  32427  itg2addnclem3  32429  itg2addnc  32430  ftc1anclem8  32458  areacirc  32471  ismtyval  32565  ismrer1  32603  grposnOLD  32647  rabeq12f  32931  csbeq12  32932  iuneq12f  32938  lsatcv1  33149  glbconN  33477  atltcvr  33535  3dim2  33568  islln2a  33617  2at0mat0  33625  islpln2a  33648  islvol2aN  33692  pmodlem2  33947  pmapjat1  33953  pcl0bN  34023  osumclN  34067  pexmidALTN  34078  lhp2at0nle  34135  4atexlemunv  34166  cdleme18b  34393  cdleme31sn1  34483  cdleme31sde  34487  cdleme31sn2  34491  ltrniotavalbN  34686  trljco  34842  cdlemh  34919  cdlemk40t  35020  cdlemk40f  35021  cdleml9  35086  dihmeetlem3N  35408  dochkrshp  35489  dihprrn  35529  dihjat1  35532  dvh3dim  35549  dochkrsm  35561  dochexmid  35571  lcfl7lem  35602  lcfl9a  35608  lclkrlem1  35609  mapdspex  35771  mapdindp2  35824  mapdh6dN  35842  hdmap1l6d  35917  hdmap11lem2  35948  hdmap14lem4a  35977  hdmapip0  36021  hlhilset  36040  jm2.26a  36381  radcnvrat  37331  sumsnd  38004  sumsnf  38433  icccncfext  38570  fperdvper  38605  dvcosax  38613  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  volioc  38661  itgiccshift  38669  stoweidlem34  38724  dirkercncflem2  38794  fourierdlem32  38829  fourierdlem41  38838  fourierdlem48  38844  fourierdlem64  38860  fourierdlem73  38869  fourierdlem79  38875  fourierdlem82  38878  fourierdlem97  38893  fourierdlem101  38897  fourierdlem109  38905  fourierdlem111  38907  fouriersw  38921  elaa2  38924  etransclem24  38948  etransclem25  38949  etransclem46  38970  nnfoctbdjlem  39145  ismeannd  39157  fzopredsuc  39744  fmtnorec2lem  39790  2pwp1prmfmtno  39840  sfprmdvdsmersenne  39856  sgprmdvdsmersenne  39857  lighneallem2  39859  lighneallem3  39860  dfodd6  39886  dfeven4  39887  m1expevenALTV  39896  usgr1vr  40476  cplgr2vpr  40650  cplgr3v  40652  cusgrrusgr  40776  1wlklenvm1  40821  1wlk0prc  40857  wlksoneq1eq2  40867  crctcsh1wlkn0lem4  41011  crctcsh1wlkn0lem5  41012  crctcsh1wlkn0lem6  41013  crctcshlem4  41018  crctcsh  41022  1wlkiswwlks1  41059  wwlksnextbi  41095  wwlksnextwrd  41098  clwlkclwwlklem2fv1  41199  clwlkclwwlklem2a4  41201  clwlkclwwlklem3  41205  clwwlksn2  41212  clwwlksf  41217  clwwlksf1  41219  wwlksext2clwwlk  41226  clwwisshclwws  41230  erclwwlkseqlen  41235  eleclclwwlksnlem2  41241  erclwwlksneqlen  41247  umgrhashecclwwlk  41257  eucrctshift  41406  eucrct2eupth  41408  fusgr2wsp2nb  41493  av-extwwlkfablem2  41505  clintopval  41625  lmod0rng  41653  2zrngagrp  41728  rngcval  41749  ringcval  41795  dmmpt2ssx2  41903  zlmodzxzscm  41923  zlmodzxzadd  41924  domnmsuppn0  41939  rmsuppss  41940  scmsuppss  41942  ply1mulgsumlem4  41966  ldepsprlem  42050  lincresunit2  42056  m1modmmod  42105  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator