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

Theorem sylan9eqr 2492
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
Hypotheses
Ref Expression
sylan9eqr.1  |-  ( ph  ->  A  =  B )
sylan9eqr.2  |-  ( ps 
->  B  =  C
)
Assertion
Ref Expression
sylan9eqr  |-  ( ( ps  /\  ph )  ->  A  =  C )

Proof of Theorem sylan9eqr
StepHypRef Expression
1 sylan9eqr.1 . . 3  |-  ( ph  ->  A  =  B )
2 sylan9eqr.2 . . 3  |-  ( ps 
->  B  =  C
)
31, 2sylan9eq 2490 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 454 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421
This theorem is referenced by:  sbcied2  3343  csbied2  3429  fun2ssres  5642  fcoi1  5774  fcoi2  5775  funssfv  5896  fvtp1  6126  nvof1o  6194  onuninsuci  6681  ot1stg  6821  ot2ndg  6822  el2xptp0  6851  mpt2mptsx  6870  dmmpt2ssx  6872  fmpt2x  6873  2ndconst  6896  mpt2xopoveq  6973  wfrlem10  7053  rdgeq12  7139  rdgsucmptnf  7155  frsucmptn  7164  oev2  7233  oesuclem  7235  oawordeulem  7263  om00  7284  omass  7289  oeoa  7306  oeoe  7308  nnmass  7333  oaabs2  7354  omabs  7356  omxpenlem  7679  sbthlem4  7691  sbthlem6  7693  fodomr  7729  ssenen  7752  fi0  7940  cantnfp1  8185  cnfcomlem  8203  cardaleph  8518  cflim2  8691  axdc4lem  8883  fpwwe2lem12  9065  fpwwe2lem13  9066  rankcf  9201  inatsk  9202  ltrnq  9403  addclprlem1  9440  mulclprlem  9443  1idpr  9453  prlem936  9471  reclem3pr  9473  mulcmpblnrlem  9493  recexsrlem  9526  map2psrpr  9533  nnnn0addcl  10900  zindd  11036  qaddcl  11280  qmulcl  11282  qreccl  11284  xaddnemnf  11527  xaddnepnf  11528  xaddcom  11531  xnegdi  11534  xaddass  11535  xpncan  11537  xleadd1a  11539  xlt2add  11546  rexmul  11557  xmulgt0  11569  xmulge0  11570  xmulasslem3  11572  xlemul1a  11574  xadddilem  11580  xadddi2  11583  modm1p1mod0  12138  seqf1olem2  12250  expp1  12276  expneg  12277  expcllem  12280  mulexp  12308  expmul  12314  bcpasc  12503  hashrabsn01  12549  fseq1hash  12552  hashinfxadd  12561  hashfzo  12596  ffzo0hash  12598  fz0hash  12608  hashf1lem1  12613  hashge2el2dif  12630  brfi1indlem  12640  lsw0  12699  ccatval1  12709  ccatval2  12710  swrdval  12758  reuccats1  12822  splval  12843  repswswrd  12872  2cshwcshw  12909  s4dom  12983  wrdlen2i  13000  shftfn  13115  reim0b  13161  cjexp  13192  sqeqd  13208  fsumser  13774  sumsn  13785  binomlem  13865  expcnv  13900  prodsn  13994  prodsnf  13996  bpolylem  14079  bpoly2  14088  bpoly3  14089  ef0lem  14111  dvdsnegb  14298  sadadd2lem2  14398  gcdabs  14471  dvdslcm  14528  lcmeq0  14530  lcmcl  14531  lcmabs  14535  lcmgcdlem  14536  lcmdvds  14538  lcmf0val  14557  lcmftp  14571  lcmfunsnlem2  14575  coprmdvds  14621  mulgcddvds  14623  pcge0  14765  pcadd  14788  pcmpt2  14792  prmreclem4  14817  ramval  14914  ramvalOLD  14915  ramcl  14941  fvprmselelfz  14956  fvprmselgcd1  14957  prmdvdsprmorOLD  14969  ressid2  15130  ressval2  15131  mrcmndind  16555  frmdval  16577  mgm2nsgrplem3  16596  mulgfval  16701  mulgnn0subcl  16713  mulgnn0z  16720  isga  16887  symgval  16962  symgextfve  17002  symgfixf1  17020  f1omvdco2  17031  psgnsn  17103  odid  17120  gexid  17159  frgpuptinv  17347  frgpup2  17352  dprdsn  17595  srgmulgass  17690  srgpcomp  17691  srgbinomlem4  17702  f1rhm0to0  17894  f1rhm0to0ALT  17895  isabvd  17974  issrng  18004  lmodvsmmulgdi  18052  mptscmfsupp0  18079  lvecinv  18262  lspdisj2  18276  lspfixed  18277  lspexch  18278  sralem  18326  srasca  18330  sravsca  18331  sraip  18332  assamulgscmlem2  18499  mplval  18578  opsrval  18624  cply1mul  18813  gsummoncoe1  18824  evl1fval  18842  znval  19028  psgndiflemB  19090  isphl  19117  scmate  19457  scmatscm  19460  mdetdiagid  19547  mdetunilem7  19565  mdetuni0  19568  gsummatr01lem3  19604  gsummatr01lem4  19605  gsummatr01  19606  slesolinvbi  19628  cpmatacl  19662  cpmatinvcl  19663  pmatcollpw2lem  19723  monmatcollpw  19725  pmatcollpwfi  19728  mp2pm2mplem4  19755  pm2mp  19771  cpmadugsumlemF  19822  cpmadugsumfi  19823  cpmadumatpoly  19829  cayhamlem4  19834  cayleyhamilton0  19835  cayleyhamiltonALT  19837  indistopon  19938  0ntr  20009  pnrmopn  20281  reftr  20451  kgenval  20472  pt1hmeo  20743  fmval  20880  fmf  20882  istmd  21011  istgp  21014  tsmsval2  21066  isxmet2d  21264  xpsxmetlem  21316  xpsmet  21319  blfvalps  21320  tmsval  21418  isnlm  21600  nmoleub  21654  idnghm  21666  blssioo  21715  blcvx  21718  icccvx  21865  pcorevlem  21941  isclm  21979  caufval  22129  iscms  22197  mbfsup  22488  i1f1  22516  dvexp3  22798  rolle  22810  dvivth  22830  deg1add  22920  0dgr  23058  coefv0  23061  elqaalem2  23132  dvradcnv  23232  abelthlem8  23250  efper  23290  logtayl  23461  abscxpbnd  23549  relogbcxpb  23580  dcubic2  23626  rlimcnp2  23748  cvxcl  23766  zetacvg  23796  lgamgulmlem2  23811  vmaval  23894  chtub  23994  logexprlim  24007  dchrsum2  24050  sumdchr2  24052  bposlem2  24067  lgsdir  24112  lgsne0  24115  lgsdirnn0  24121  lgsdinn0  24122  lgsquadlem2  24137  dchrvmasum2if  24189  dchrvmasumiflem1  24193  rpvmasum2  24204  pntpbnd1  24278  ostth2lem4  24328  trgcgrg  24413  ax5seglem1  24795  ax5seglem2  24796  ax5seglem5  24800  usgraedgprv  24940  wwlknimp  25251  wwlknextbi  25289  wwlkextwrd  25292  clwlkisclwwlklem2fv1  25346  clwlkisclwwlklem2a4  25348  clwlkisclwwlklem0  25352  clwwlkf  25358  clwwlkf1  25360  wwlkext2clwwlk  25367  clwwisshclww  25371  erclwwlkeqlen  25376  eleclclwwlknlem2  25382  erclwwlkneqlen  25388  usghashecclwwlk  25399  vdgr1d  25467  vdgr1b  25468  vdgr1a  25470  cusgraisrusgra  25502  rusgra0edg  25519  eupatrl  25532  usg2spot2nb  25629  grpoidinvlem2  25769  grposn  25779  gxnn0neg  25827  gxid  25837  vcz  26025  nvz  26134  lnon0  26275  ipasslem2  26309  htthlem  26396  hvpncan  26518  hiidge0  26577  normgt0  26606  hsn0elch  26727  shsel3  26794  spansneleq  27049  normcan  27055  h1datomi  27060  fh1  27097  spansncvi  27131  5oalem1  27133  5oalem3  27135  5oalem5  27137  3oalem2  27142  pjdsi  27191  kbpj  27435  0hmop  27462  0lnfn  27464  adj0  27473  nlelshi  27539  branmfn  27584  opsqrlem1  27619  hst1h  27706  mdsl0  27789  superpos  27833  sumdmdlem  27897  cdj3lem1  27913  xrpxdivcld  28233  2sqn0  28236  xrge0npcan  28286  resvid2  28421  resvval2  28422  esumsnf  28715  esummulc1  28732  measxun2  28862  omsmeas  28975  sibfof  28992  probun  29069  bnj517  29475  mrsubfval  29925  msrval  29955  subdivcomb2  30139  dfrdg2  30220  bj-bary1lem1  31452  poimirlem1  31635  poimirlem2  31636  poimirlem3  31637  poimirlem4  31638  poimirlem5  31639  poimirlem6  31640  poimirlem7  31641  poimirlem10  31644  poimirlem11  31645  poimirlem12  31646  poimirlem14  31648  poimirlem15  31649  poimirlem17  31651  poimirlem20  31654  poimirlem22  31656  poimirlem23  31657  poimirlem24  31658  poimirlem25  31659  poimirlem26  31660  poimirlem27  31661  mblfinlem2  31672  mblfinlem3  31673  ismblfin  31675  mbfposadd  31682  itg2addnclem  31687  itg2addnclem3  31689  itg2addnc  31690  ftc1anclem8  31718  areacirc  31731  ismtyval  31826  ismrer1  31864  rabeq12f  32094  csbeq12  32095  iuneq12f  32101  lsatcv1  32313  glbconN  32641  atltcvr  32699  3dim2  32732  islln2a  32781  2at0mat0  32789  islpln2a  32812  islvol2aN  32856  pmodlem2  33111  pmapjat1  33117  pcl0bN  33187  osumclN  33231  pexmidALTN  33242  lhp2at0nle  33299  4atexlemunv  33330  cdleme18b  33557  cdleme31sn1  33647  cdleme31sde  33651  cdleme31sn2  33655  ltrniotavalbN  33850  trljco  34006  cdlemh  34083  cdlemk40t  34184  cdlemk40f  34185  cdleml9  34250  dihmeetlem3N  34572  dochkrshp  34653  dihprrn  34693  dihjat1  34696  dvh3dim  34713  dochkrsm  34725  dochexmid  34735  lcfl7lem  34766  lcfl9a  34772  lclkrlem1  34773  mapdspex  34935  mapdindp2  34988  mapdh6dN  35006  hdmap1l6d  35081  hdmap11lem2  35112  hdmap14lem4a  35141  hdmapip0  35185  hlhilset  35204  bezoutr1  35532  jm2.26a  35551  radcnvrat  36290  sumsnd  36977  sumsnf  37213  icccncfext  37327  fperdvper  37352  dvcosax  37360  ioodvbdlimc1lem1  37365  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  volioc  37408  itgiccshift  37416  stoweidlem34  37454  dirkercncflem2  37525  fourierdlem32  37560  fourierdlem41  37569  fourierdlem48  37576  fourierdlem64  37592  fourierdlem73  37601  fourierdlem79  37607  fourierdlem82  37610  fourierdlem97  37625  fourierdlem101  37629  fourierdlem109  37637  fourierdlem111  37639  fouriersw  37653  etransclem24  37680  etransclem25  37681  etransclem46  37702  ismeannd  37804  fzopredsuc  38100  mod2eq1n2dvds  38105  dfodd6  38147  dfeven4  38148  m1expevenALTV  38157  vdcusgra  38419  clintopval  38588  lmod0rng  38616  2zrngagrp  38691  rngcval  38712  ringcval  38758  dmmpt2ssx2  38868  zlmodzxzscm  38888  zlmodzxzadd  38889  domnmsuppn0  38904  rmsuppss  38905  scmsuppss  38907  ply1mulgsumlem4  38931  ldepsprlem  39015  lincresunit2  39021  m1modmmod  39075  nn0sumshdiglemB  39182
  Copyright terms: Public domain W3C validator