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

Theorem sylan9eqr 2826
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 2824 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 455 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852  df-cleq 2763
This theorem is referenced by:  sbcied2  3623  csbied2  3708  opthhausdorff0  5111  fun2ssres  6074  fcoi1  6218  fcoi2  6219  funssfv  6350  fvtp1  6603  nvof1o  6678  onuninsuci  7186  ot1stg  7328  ot2ndg  7329  el2xptp0  7360  mpt2mptsx  7382  dmmpt2ssx  7384  fmpt2x  7385  2ndconst  7416  mpt2xopoveq  7496  wfrlem10  7576  rdgeq12  7661  rdgsucmptnf  7677  frsucmptn  7686  oev2  7756  oesuclem  7758  oawordeulem  7787  om00  7808  omass  7813  oeoa  7830  oeoe  7832  nnmass  7857  oaabs2  7878  omabs  7880  omxpenlem  8216  sbthlem4  8228  sbthlem6  8230  fodomr  8266  ssenen  8289  fi0  8481  cantnfp1  8741  cnfcomlem  8759  cardaleph  9111  cflim2  9286  axdc4lem  9478  fpwwe2lem12  9664  fpwwe2lem13  9665  rankcf  9800  inatsk  9801  ltrnq  10002  addclprlem1  10039  mulclprlem  10042  1idpr  10052  prlem936  10070  reclem3pr  10072  mulcmpblnrlem  10092  recexsrlem  10125  map2psrpr  10132  addid0  10651  nnnn0addcl  11524  zindd  11679  qaddcl  12006  qmulcl  12008  qreccl  12010  xaddnemnf  12271  xaddnepnf  12272  xaddcom  12275  xnegdi  12282  xaddass  12283  xpncan  12285  xleadd1a  12287  xlt2add  12294  rexmul  12305  xmulgt0  12317  xmulge0  12318  xmulasslem3  12320  xlemul1a  12322  xadddilem  12328  xadddi2  12331  modmuladd  12919  modm1p1mod0  12928  modfzo0difsn  12949  seqf1olem2  13047  expp1  13073  expneg  13074  expcllem  13077  mulexp  13105  expmul  13111  sqoddm1div8  13234  bcpasc  13311  hashrabsn01  13363  fseq1hash  13366  hashinfxadd  13375  hashfzo  13417  fnfz0hash  13431  ffzo0hash  13434  hashf1lem1  13440  hashge2el2dif  13463  hashdifsnp1  13479  lsw0  13548  ccatval1  13558  ccatval2  13559  swrdval  13624  reuccats1  13688  splval  13710  repswswrd  13739  2cshwcshw  13779  s4dom  13872  wrdlen2i  13895  shftfn  14020  reim0b  14066  cjexp  14097  sqeqd  14113  fsumser  14668  sumsnf  14680  sumsn  14682  binomlem  14767  expcnv  14802  prodsn  14898  prodsnf  14900  bpolylem  14984  bpoly2  14993  bpoly3  14994  ef0lem  15014  dvdsnegb  15207  mod2eq1n2dvds  15278  m1expe  15298  m1expo  15299  m1exp1  15300  flodddiv4  15344  sadadd2lem2  15379  gcdabs  15457  bezoutr1  15489  dvdslcm  15518  lcmeq0  15520  lcmcl  15521  lcmabs  15525  lcmgcdlem  15526  lcmdvds  15528  lcmf0val  15542  lcmftp  15556  lcmfunsnlem2  15560  mulgcddvds  15575  divgcdcoprmex  15586  pcge0  15772  pcadd  15799  pcmpt2  15803  prmreclem4  15829  ramval  15918  ramcl  15939  fvprmselelfz  15954  fvprmselgcd1  15955  ressid2  16134  ressval2  16135  mrcmndind  17573  frmdval  17595  mgm2nsgrplem3  17614  mulgfval  17749  mulgnn0subcl  17761  mulgnn0z  17774  isga  17930  symgval  18005  symgextfve  18045  symgfixf1  18063  f1omvdco2  18074  psgnsn  18146  odid  18163  gexid  18202  frgpuptinv  18390  frgpup2  18395  dprdsn  18642  srgmulgass  18738  srgpcomp  18739  srgbinomlem4  18750  ringinvnzdiv  18800  f1rhm0to0  18949  f1rhm0to0ALT  18950  isabvd  19029  issrng  19059  lmodvsmmulgdi  19107  mptscmfsupp0  19137  lvecinv  19325  lspdisj2  19339  lspfixed  19340  lspfixedOLD  19341  lspexch  19342  sralem  19391  srasca  19395  sravsca  19396  sraip  19397  assamulgscmlem2  19563  mplval  19642  opsrval  19688  cply1mul  19878  gsummoncoe1  19888  evl1fval  19906  znval  20097  psgndiflemB  20161  isphl  20189  scmate  20533  scmatscm  20536  mdetdiagid  20623  mdetunilem7  20641  mdetuni0  20644  gsummatr01lem3  20681  gsummatr01lem4  20682  gsummatr01  20683  slesolinvbi  20705  cpmatacl  20740  cpmatinvcl  20741  pmatcollpw2lem  20801  monmatcollpw  20803  pmatcollpwfi  20806  mp2pm2mplem4  20833  pm2mp  20849  cpmadugsumlemF  20900  cpmadugsumfi  20901  cpmadumatpoly  20907  cayhamlem4  20912  cayleyhamilton0  20913  cayleyhamiltonALT  20915  indistopon  21025  0ntr  21095  pnrmopn  21367  reftr  21537  kgenval  21558  pt1hmeo  21829  fmval  21966  fmf  21968  istmd  22097  istgp  22100  tsmsval2  22152  isxmet2d  22351  xpsxmetlem  22403  xpsmet  22406  blfvalps  22407  tmsval  22505  isnlm  22698  nmoleub  22754  idnghm  22766  blssioo  22817  blcvx  22820  icccvx  22968  pcorevlem  23044  isclm  23082  caufval  23291  iscms  23360  mbfsup  23650  i1f1  23676  dvexp3  23960  rolle  23972  dvivth  23992  deg1add  24082  0dgr  24220  coefv0  24223  elqaalem2  24294  dvradcnv  24394  abelthlem8  24412  efper  24451  logtayl  24626  abscxpbnd  24714  relogbcxpb  24745  dcubic2  24791  rlimcnp2  24913  cvxcl  24931  zetacvg  24961  lgamgulmlem2  24976  vmaval  25059  chtub  25157  logexprlim  25170  dchrsum2  25213  sumdchr2  25215  bposlem2  25230  lgsdir  25277  lgsne0  25280  lgsdirnn0  25289  lgsdinn0  25290  lgsquadlem2  25326  2lgslem3a  25341  2lgslem3b  25342  2lgslem3c  25343  2lgslem3d  25344  2lgslem3a1  25345  2lgslem3b1  25346  2lgslem3c1  25347  2lgslem3d1  25348  dchrvmasum2if  25406  dchrvmasumiflem1  25410  rpvmasum2  25421  pntpbnd1  25495  ostth2lem4  25545  trgcgrg  25630  ax5seglem1  26028  ax5seglem2  26029  ax5seglem5  26033  usgr1vr  26369  cplgr2vpr  26563  cplgr3v  26565  cusgrrusgr  26711  wlklenvm1  26751  wlk0prc  26784  wlksoneq1eq2  26794  crctcshwlkn0lem4  26940  crctcshwlkn0lem5  26941  crctcshwlkn0lem6  26942  crctcshlem4  26947  crctcsh  26951  wlkiswwlks1  27000  wwlksnextbi  27036  wwlksnextwrd  27039  midwwlks2s3  27096  clwlkclwwlklem2fv1  27142  clwlkclwwlklem2a4  27144  clwlkclwwlklem3  27148  clwwisshclwws  27162  erclwwlkeqlen  27166  clwwlkinwwlk  27193  clwwlkn2  27197  clwwlkf  27200  clwwlkf1  27202  wwlksext2clwwlkOLD  27212  eleclclwwlknlem2  27216  erclwwlkneqlen  27223  umgrhashecclwwlk  27233  eucrctshift  27420  eucrct2eupth  27422  fusgr2wsp2nb  27513  grpoidinvlem2  27693  vcz  27764  nvz  27858  lnon0  27987  ipasslem2  28021  htthlem  28108  hvpncan  28230  hiidge0  28289  normgt0  28318  hsn0elch  28439  shsel3  28508  spansneleq  28763  normcan  28769  h1datomi  28774  fh1  28811  spansncvi  28845  5oalem1  28847  5oalem3  28849  5oalem5  28851  3oalem2  28856  pjdsi  28905  kbpj  29149  0hmop  29176  0lnfn  29178  adj0  29187  nlelshi  29253  branmfn  29298  opsqrlem1  29333  hst1h  29420  mdsl0  29503  superpos  29547  sumdmdlem  29611  cdj3lem1  29627  f1od2  29833  xrpxdivcld  29977  2sqn0  29980  xrge0npcan  30028  resvid2  30162  resvval2  30163  esumsnf  30460  esummulc1  30477  measxun2  30607  omsmeas  30719  sibfof  30736  probun  30815  bnj517  31287  mrsubfval  31737  msrval  31767  subdivcomb2  31944  dfrdg2  32031  bj-bary1lem1  33491  rdgeqoa  33548  finxpreclem2  33557  finxpreclem3  33560  matunitlindflem1  33731  poimirlem1  33736  poimirlem2  33737  poimirlem3  33738  poimirlem4  33739  poimirlem5  33740  poimirlem6  33741  poimirlem7  33742  poimirlem10  33745  poimirlem11  33746  poimirlem12  33747  poimirlem14  33749  poimirlem15  33750  poimirlem17  33752  poimirlem20  33755  poimirlem22  33757  poimirlem23  33758  poimirlem24  33759  poimirlem25  33760  poimirlem26  33761  poimirlem27  33762  mblfinlem2  33773  mblfinlem3  33774  ismblfin  33776  mbfposadd  33782  itg2addnclem  33786  itg2addnclem3  33788  itg2addnc  33789  ftc1anclem8  33817  areacirc  33830  ismtyval  33924  ismrer1  33962  grposnOLD  34006  rabeq12f  34290  csbeq12  34291  iuneq12f  34297  lsatcv1  34850  glbconN  35178  atltcvr  35236  3dim2  35269  islln2a  35318  2at0mat0  35326  islpln2a  35349  islvol2aN  35393  pmodlem2  35648  pmapjat1  35654  pcl0bN  35724  osumclN  35768  pexmidALTN  35779  lhp2at0nle  35836  4atexlemunv  35867  cdleme18b  36094  cdleme31sn1  36183  cdleme31sde  36187  cdleme31sn2  36191  ltrniotavalbN  36386  trljco  36542  cdlemh  36619  cdlemk40t  36720  cdlemk40f  36721  cdleml9  36786  dihmeetlem3N  37108  dochkrshp  37189  dihprrn  37229  dihjat1  37232  dvh3dim  37249  dochkrsm  37261  dochexmid  37271  lcfl7lem  37302  lcfl9a  37308  lclkrlem1  37309  mapdspex  37471  mapdindp2  37524  mapdh6dN  37542  hdmap1l6d  37616  hdmap11lem2  37645  hdmap14lem4a  37674  hdmapip0  37718  hlhilset  37737  jm2.26a  38086  radcnvrat  39032  sumsnd  39701  icccncfext  40612  fperdvper  40645  dvcosax  40653  ioodvbdlimc1lem1  40658  ioodvbdlimc1lem2  40659  ioodvbdlimc2lem  40661  volioc  40699  itgiccshift  40707  stoweidlem34  40762  dirkercncflem2  40832  fourierdlem32  40867  fourierdlem41  40876  fourierdlem48  40882  fourierdlem64  40898  fourierdlem73  40907  fourierdlem79  40913  fourierdlem82  40916  fourierdlem97  40931  fourierdlem101  40935  fourierdlem109  40943  fourierdlem111  40945  fouriersw  40959  elaa2  40962  etransclem24  40986  etransclem25  40987  etransclem46  41008  nnfoctbdjlem  41183  ismeannd  41195  fzopredsuc  41851  fmtnorec2lem  41972  2pwp1prmfmtno  42022  sfprmdvdsmersenne  42038  sgprmdvdsmersenne  42039  lighneallem2  42041  lighneallem3  42042  dfodd6  42068  dfeven4  42069  m1expevenALTV  42078  clintopval  42358  lmod0rng  42386  2zrngagrp  42461  rngcval  42480  ringcval  42526  dmmpt2ssx2  42633  zlmodzxzscm  42653  zlmodzxzadd  42654  domnmsuppn0  42668  rmsuppss  42669  scmsuppss  42671  ply1mulgsumlem4  42695  ldepsprlem  42779  lincresunit2  42785  m1modmmod  42834  nn0sumshdiglemB  42932  0setrec  42968
  Copyright terms: Public domain W3C validator