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

Theorem sylan9eqr 2676
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 2674 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 469 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613
This theorem is referenced by:  sbcied2  3467  csbied2  3554  fun2ssres  5919  fcoi1  6065  fcoi2  6066  funssfv  6196  fvtp1  6445  nvof1o  6521  onuninsuci  7025  ot1stg  7167  ot2ndg  7168  el2xptp0  7197  mpt2mptsx  7218  dmmpt2ssx  7220  fmpt2x  7221  2ndconst  7251  mpt2xopoveq  7330  wfrlem10  7409  rdgeq12  7494  rdgsucmptnf  7510  frsucmptn  7519  oev2  7588  oesuclem  7590  oawordeulem  7619  om00  7640  omass  7645  oeoa  7662  oeoe  7664  nnmass  7689  oaabs2  7710  omabs  7712  omxpenlem  8046  sbthlem4  8058  sbthlem6  8060  fodomr  8096  ssenen  8119  fi0  8311  cantnfp1  8563  cnfcomlem  8581  cardaleph  8897  cflim2  9070  axdc4lem  9262  fpwwe2lem12  9448  fpwwe2lem13  9449  rankcf  9584  inatsk  9585  ltrnq  9786  addclprlem1  9823  mulclprlem  9826  1idpr  9836  prlem936  9854  reclem3pr  9856  mulcmpblnrlem  9876  recexsrlem  9909  map2psrpr  9916  addid0  10435  nnnn0addcl  11308  zindd  11463  qaddcl  11789  qmulcl  11791  qreccl  11793  xaddnemnf  12052  xaddnepnf  12053  xaddcom  12056  xnegdi  12063  xaddass  12064  xpncan  12066  xleadd1a  12068  xlt2add  12075  rexmul  12086  xmulgt0  12098  xmulge0  12099  xmulasslem3  12101  xlemul1a  12103  xadddilem  12109  xadddi2  12112  modmuladd  12695  modm1p1mod0  12704  modfzo0difsn  12725  seqf1olem2  12824  expp1  12850  expneg  12851  expcllem  12854  mulexp  12882  expmul  12888  sqoddm1div8  13011  bcpasc  13091  hashrabsn01  13145  fseq1hash  13148  hashinfxadd  13157  hashfzo  13199  fnfz0hash  13213  ffzo0hash  13216  hashf1lem1  13222  hashge2el2dif  13245  brfi1indlem  13261  lsw0  13335  ccatval1  13344  ccatval2  13345  swrdval  13399  reuccats1  13462  splval  13483  repswswrd  13512  2cshwcshw  13552  s4dom  13645  wrdlen2i  13667  shftfn  13794  reim0b  13840  cjexp  13871  sqeqd  13887  fsumser  14442  sumsnf  14454  sumsn  14456  binomlem  14542  expcnv  14577  prodsn  14673  prodsnf  14675  bpolylem  14760  bpoly2  14769  bpoly3  14770  ef0lem  14790  dvdsnegb  14980  mod2eq1n2dvds  15052  m1expe  15072  m1expo  15073  m1exp1  15074  flodddiv4  15118  sadadd2lem2  15153  gcdabs  15231  bezoutr1  15263  dvdslcm  15292  lcmeq0  15294  lcmcl  15295  lcmabs  15299  lcmgcdlem  15300  lcmdvds  15302  lcmf0val  15316  lcmftp  15330  lcmfunsnlem2  15334  coprmdvdsOLD  15348  mulgcddvds  15350  divgcdcoprmex  15361  pcge0  15547  pcadd  15574  pcmpt2  15578  prmreclem4  15604  ramval  15693  ramcl  15714  fvprmselelfz  15729  fvprmselgcd1  15730  ressid2  15909  ressval2  15910  mrcmndind  17347  frmdval  17369  mgm2nsgrplem3  17388  mulgfval  17523  mulgnn0subcl  17535  mulgnn0z  17548  isga  17705  symgval  17780  symgextfve  17820  symgfixf1  17838  f1omvdco2  17849  psgnsn  17921  odid  17938  gexid  17977  frgpuptinv  18165  frgpup2  18170  dprdsn  18416  srgmulgass  18512  srgpcomp  18513  srgbinomlem4  18524  ringinvnzdiv  18574  f1rhm0to0  18721  f1rhm0to0ALT  18722  isabvd  18801  issrng  18831  lmodvsmmulgdi  18879  mptscmfsupp0  18909  lvecinv  19094  lspdisj2  19108  lspfixed  19109  lspexch  19110  sralem  19158  srasca  19162  sravsca  19163  sraip  19164  assamulgscmlem2  19330  mplval  19409  opsrval  19455  cply1mul  19645  gsummoncoe1  19655  evl1fval  19673  znval  19864  psgndiflemB  19927  isphl  19954  scmate  20297  scmatscm  20300  mdetdiagid  20387  mdetunilem7  20405  mdetuni0  20408  gsummatr01lem3  20444  gsummatr01lem4  20445  gsummatr01  20446  slesolinvbi  20468  cpmatacl  20502  cpmatinvcl  20503  pmatcollpw2lem  20563  monmatcollpw  20565  pmatcollpwfi  20568  mp2pm2mplem4  20595  pm2mp  20611  cpmadugsumlemF  20662  cpmadugsumfi  20663  cpmadumatpoly  20669  cayhamlem4  20674  cayleyhamilton0  20675  cayleyhamiltonALT  20677  indistopon  20786  0ntr  20856  pnrmopn  21128  reftr  21298  kgenval  21319  pt1hmeo  21590  fmval  21728  fmf  21730  istmd  21859  istgp  21862  tsmsval2  21914  isxmet2d  22113  xpsxmetlem  22165  xpsmet  22168  blfvalps  22169  tmsval  22267  isnlm  22460  nmoleub  22516  idnghm  22528  blssioo  22579  blcvx  22582  icccvx  22730  pcorevlem  22807  isclm  22845  caufval  23054  iscms  23123  mbfsup  23412  i1f1  23438  dvexp3  23722  rolle  23734  dvivth  23754  deg1add  23844  0dgr  23982  coefv0  23985  elqaalem2  24056  dvradcnv  24156  abelthlem8  24174  efper  24212  logtayl  24387  abscxpbnd  24475  relogbcxpb  24506  dcubic2  24552  rlimcnp2  24674  cvxcl  24692  zetacvg  24722  lgamgulmlem2  24737  vmaval  24820  chtub  24918  logexprlim  24931  dchrsum2  24974  sumdchr2  24976  bposlem2  24991  lgsdir  25038  lgsne0  25041  lgsdirnn0  25050  lgsdinn0  25051  lgsquadlem2  25087  2lgslem3a  25102  2lgslem3b  25103  2lgslem3c  25104  2lgslem3d  25105  2lgslem3a1  25106  2lgslem3b1  25107  2lgslem3c1  25108  2lgslem3d1  25109  dchrvmasum2if  25167  dchrvmasumiflem1  25171  rpvmasum2  25182  pntpbnd1  25256  ostth2lem4  25306  trgcgrg  25391  ax5seglem1  25789  ax5seglem2  25790  ax5seglem5  25794  usgr1vr  26128  cplgr2vpr  26310  cplgr3v  26312  cusgrrusgr  26458  wlklenvm1  26498  wlk0prc  26531  wlksoneq1eq2  26541  crctcshwlkn0lem4  26686  crctcshwlkn0lem5  26687  crctcshwlkn0lem6  26688  crctcshlem4  26693  crctcsh  26697  wlkiswwlks1  26734  wwlksnextbi  26770  wwlksnextwrd  26773  midwwlks2s3  26841  clwlkclwwlklem2fv1  26877  clwlkclwwlklem2a4  26879  clwlkclwwlklem3  26883  clwwlksn2  26890  clwwlksf  26895  clwwlksf1  26897  wwlksext2clwwlk  26904  clwwisshclwws  26908  erclwwlkseqlen  26913  eleclclwwlksnlem2  26919  erclwwlksneqlen  26925  umgrhashecclwwlk  26935  eucrctshift  27083  eucrct2eupth  27085  fusgr2wsp2nb  27172  extwwlkfablem2  27184  grpoidinvlem2  27329  vcz  27400  nvz  27494  lnon0  27623  ipasslem2  27657  htthlem  27744  hvpncan  27866  hiidge0  27925  normgt0  27954  hsn0elch  28075  shsel3  28144  spansneleq  28399  normcan  28405  h1datomi  28410  fh1  28447  spansncvi  28481  5oalem1  28483  5oalem3  28485  5oalem5  28487  3oalem2  28492  pjdsi  28541  kbpj  28785  0hmop  28812  0lnfn  28814  adj0  28823  nlelshi  28889  branmfn  28934  opsqrlem1  28969  hst1h  29056  mdsl0  29139  superpos  29183  sumdmdlem  29247  cdj3lem1  29263  xrpxdivcld  29617  2sqn0  29620  xrge0npcan  29668  resvid2  29802  resvval2  29803  esumsnf  30100  esummulc1  30117  measxun2  30247  omsmeas  30359  sibfof  30376  probun  30455  bnj517  30929  mrsubfval  31379  msrval  31409  subdivcomb2  31587  dfrdg2  31675  bj-bary1lem1  33132  rdgeqoa  33189  finxpreclem2  33198  finxpreclem3  33201  matunitlindflem1  33376  poimirlem1  33381  poimirlem2  33382  poimirlem3  33383  poimirlem4  33384  poimirlem5  33385  poimirlem6  33386  poimirlem7  33387  poimirlem10  33390  poimirlem11  33391  poimirlem12  33392  poimirlem14  33394  poimirlem15  33395  poimirlem17  33397  poimirlem20  33400  poimirlem22  33402  poimirlem23  33403  poimirlem24  33404  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  mblfinlem2  33418  mblfinlem3  33419  ismblfin  33421  mbfposadd  33428  itg2addnclem  33432  itg2addnclem3  33434  itg2addnc  33435  ftc1anclem8  33463  areacirc  33476  ismtyval  33570  ismrer1  33608  grposnOLD  33652  rabeq12f  33936  csbeq12  33937  iuneq12f  33943  lsatcv1  34154  glbconN  34482  atltcvr  34540  3dim2  34573  islln2a  34622  2at0mat0  34630  islpln2a  34653  islvol2aN  34697  pmodlem2  34952  pmapjat1  34958  pcl0bN  35028  osumclN  35072  pexmidALTN  35083  lhp2at0nle  35140  4atexlemunv  35171  cdleme18b  35398  cdleme31sn1  35488  cdleme31sde  35492  cdleme31sn2  35496  ltrniotavalbN  35691  trljco  35847  cdlemh  35924  cdlemk40t  36025  cdlemk40f  36026  cdleml9  36091  dihmeetlem3N  36413  dochkrshp  36494  dihprrn  36534  dihjat1  36537  dvh3dim  36554  dochkrsm  36566  dochexmid  36576  lcfl7lem  36607  lcfl9a  36613  lclkrlem1  36614  mapdspex  36776  mapdindp2  36829  mapdh6dN  36847  hdmap1l6d  36922  hdmap11lem2  36953  hdmap14lem4a  36982  hdmapip0  37026  hlhilset  37045  jm2.26a  37386  radcnvrat  38333  sumsnd  39005  icccncfext  39863  fperdvper  39896  dvcosax  39904  ioodvbdlimc1lem1  39909  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  volioc  39951  itgiccshift  39959  stoweidlem34  40014  dirkercncflem2  40084  fourierdlem32  40119  fourierdlem41  40128  fourierdlem48  40134  fourierdlem64  40150  fourierdlem73  40159  fourierdlem79  40165  fourierdlem82  40168  fourierdlem97  40183  fourierdlem101  40187  fourierdlem109  40195  fourierdlem111  40197  fouriersw  40211  elaa2  40214  etransclem24  40238  etransclem25  40239  etransclem46  40260  nnfoctbdjlem  40435  ismeannd  40447  fzopredsuc  41096  fmtnorec2lem  41219  2pwp1prmfmtno  41269  sfprmdvdsmersenne  41285  sgprmdvdsmersenne  41286  lighneallem2  41288  lighneallem3  41289  dfodd6  41315  dfeven4  41316  m1expevenALTV  41325  clintopval  41605  lmod0rng  41633  2zrngagrp  41708  rngcval  41727  ringcval  41773  dmmpt2ssx2  41880  zlmodzxzscm  41900  zlmodzxzadd  41901  domnmsuppn0  41915  rmsuppss  41916  scmsuppss  41918  ply1mulgsumlem4  41942  ldepsprlem  42026  lincresunit2  42032  m1modmmod  42081  nn0sumshdiglemB  42179  0setrec  42212
  Copyright terms: Public domain W3C validator