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

Theorem sylan9eqr 2517
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 2515 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 459 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-cleq 2454
This theorem is referenced by:  sbcied2  3316  csbied2  3402  fun2ssres  5641  fcoi1  5779  fcoi2  5780  funssfv  5902  fvtp1  6134  nvof1o  6203  onuninsuci  6693  ot1stg  6833  ot2ndg  6834  el2xptp0  6863  mpt2mptsx  6882  dmmpt2ssx  6884  fmpt2x  6885  2ndconst  6911  mpt2xopoveq  6991  wfrlem10  7070  rdgeq12  7156  rdgsucmptnf  7172  frsucmptn  7181  oev2  7250  oesuclem  7252  oawordeulem  7280  om00  7301  omass  7306  oeoa  7323  oeoe  7325  nnmass  7350  oaabs2  7371  omabs  7373  omxpenlem  7698  sbthlem4  7710  sbthlem6  7712  fodomr  7748  ssenen  7771  fi0  7959  cantnfp1  8211  cnfcomlem  8229  cardaleph  8545  cflim2  8718  axdc4lem  8910  fpwwe2lem12  9091  fpwwe2lem13  9092  rankcf  9227  inatsk  9228  ltrnq  9429  addclprlem1  9466  mulclprlem  9469  1idpr  9479  prlem936  9497  reclem3pr  9499  mulcmpblnrlem  9519  recexsrlem  9552  map2psrpr  9559  addid0  10066  nnnn0addcl  10928  zindd  11064  qaddcl  11308  qmulcl  11310  qreccl  11312  xaddnemnf  11555  xaddnepnf  11556  xaddcom  11559  xnegdi  11562  xaddass  11563  xpncan  11565  xleadd1a  11567  xlt2add  11574  rexmul  11585  xmulgt0  11597  xmulge0  11598  xmulasslem3  11600  xlemul1a  11602  xadddilem  11608  xadddi2  11611  modm1p1mod0  12172  seqf1olem2  12284  expp1  12310  expneg  12311  expcllem  12314  mulexp  12342  expmul  12348  bcpasc  12537  hashrabsn01  12583  fseq1hash  12586  hashinfxadd  12595  hashfzo  12633  ffzo0hash  12635  fz0hash  12645  hashf1lem1  12650  hashge2el2dif  12669  brfi1indlem  12681  lsw0  12747  ccatval1  12757  ccatval2  12758  swrdval  12809  reuccats1  12873  splval  12894  repswswrd  12923  2cshwcshw  12960  s4dom  13049  wrdlen2i  13066  shftfn  13184  reim0b  13230  cjexp  13261  sqeqd  13277  fsumser  13844  sumsn  13855  binomlem  13935  expcnv  13970  prodsn  14064  prodsnf  14066  bpolylem  14149  bpoly2  14158  bpoly3  14159  ef0lem  14181  dvdsnegb  14368  sadadd2lem2  14472  gcdabs  14545  dvdslcm  14611  lcmeq0  14613  lcmcl  14614  lcmabs  14618  lcmgcdlem  14619  lcmdvds  14621  lcmf0val  14640  lcmftp  14657  lcmfunsnlem2  14661  coprmdvds  14707  mulgcddvds  14709  pcge0  14859  pcadd  14882  pcmpt2  14886  prmreclem4  14911  ramval  15008  ramvalOLD  15009  ramcl  15035  fvprmselelfz  15050  fvprmselgcd1  15051  prmdvdsprmorOLD  15063  ressid2  15225  ressval2  15226  mrcmndind  16661  frmdval  16683  mgm2nsgrplem3  16702  mulgfval  16807  mulgnn0subcl  16819  mulgnn0z  16826  isga  16993  symgval  17068  symgextfve  17108  symgfixf1  17126  f1omvdco2  17137  psgnsn  17209  odid  17235  odidOLD  17251  gexid  17280  frgpuptinv  17469  frgpup2  17474  dprdsn  17717  srgmulgass  17812  srgpcomp  17813  srgbinomlem4  17824  f1rhm0to0  18016  f1rhm0to0ALT  18017  isabvd  18096  issrng  18126  lmodvsmmulgdi  18174  mptscmfsupp0  18201  lvecinv  18384  lspdisj2  18398  lspfixed  18399  lspexch  18400  sralem  18448  srasca  18452  sravsca  18453  sraip  18454  assamulgscmlem2  18621  mplval  18700  opsrval  18746  cply1mul  18935  gsummoncoe1  18946  evl1fval  18964  znval  19154  psgndiflemB  19216  isphl  19243  scmate  19583  scmatscm  19586  mdetdiagid  19673  mdetunilem7  19691  mdetuni0  19694  gsummatr01lem3  19730  gsummatr01lem4  19731  gsummatr01  19732  slesolinvbi  19754  cpmatacl  19788  cpmatinvcl  19789  pmatcollpw2lem  19849  monmatcollpw  19851  pmatcollpwfi  19854  mp2pm2mplem4  19881  pm2mp  19897  cpmadugsumlemF  19948  cpmadugsumfi  19949  cpmadumatpoly  19955  cayhamlem4  19960  cayleyhamilton0  19961  cayleyhamiltonALT  19963  indistopon  20064  0ntr  20135  pnrmopn  20407  reftr  20577  kgenval  20598  pt1hmeo  20869  fmval  21006  fmf  21008  istmd  21137  istgp  21140  tsmsval2  21192  isxmet2d  21390  xpsxmetlem  21442  xpsmet  21445  blfvalps  21446  tmsval  21544  isnlm  21726  nmoleub  21784  nmoleubOLD  21800  idnghm  21812  blssioo  21861  blcvx  21864  icccvx  22026  pcorevlem  22105  isclm  22143  caufval  22293  iscms  22361  mbfsup  22668  i1f1  22696  dvexp3  22978  rolle  22990  dvivth  23010  deg1add  23100  0dgr  23247  coefv0  23250  elqaalem2  23321  elqaalem2OLD  23324  dvradcnv  23424  abelthlem8  23442  efper  23482  logtayl  23653  abscxpbnd  23741  relogbcxpb  23772  dcubic2  23818  rlimcnp2  23940  cvxcl  23958  zetacvg  23988  lgamgulmlem2  24003  vmaval  24088  chtub  24188  logexprlim  24201  dchrsum2  24244  sumdchr2  24246  bposlem2  24261  lgsdir  24306  lgsne0  24309  lgsdirnn0  24315  lgsdinn0  24316  lgsquadlem2  24331  dchrvmasum2if  24383  dchrvmasumiflem1  24387  rpvmasum2  24398  pntpbnd1  24472  ostth2lem4  24522  trgcgrg  24608  ax5seglem1  25006  ax5seglem2  25007  ax5seglem5  25011  usgraedgprv  25151  wwlknimp  25463  wwlknextbi  25501  wwlkextwrd  25504  clwlkisclwwlklem2fv1  25558  clwlkisclwwlklem2a4  25560  clwlkisclwwlklem0  25564  clwwlkf  25570  clwwlkf1  25572  wwlkext2clwwlk  25579  clwwisshclww  25583  erclwwlkeqlen  25588  eleclclwwlknlem2  25594  erclwwlkneqlen  25600  usghashecclwwlk  25611  vdgr1d  25679  vdgr1b  25680  vdgr1a  25682  cusgraisrusgra  25714  rusgra0edg  25731  eupatrl  25744  usg2spot2nb  25841  grpoidinvlem2  25981  grposn  25991  gxnn0neg  26039  gxid  26049  vcz  26237  nvz  26346  lnon0  26487  ipasslem2  26521  htthlem  26618  hvpncan  26740  hiidge0  26799  normgt0  26828  hsn0elch  26949  shsel3  27016  spansneleq  27271  normcan  27277  h1datomi  27282  fh1  27319  spansncvi  27353  5oalem1  27355  5oalem3  27357  5oalem5  27359  3oalem2  27364  pjdsi  27413  kbpj  27657  0hmop  27684  0lnfn  27686  adj0  27695  nlelshi  27761  branmfn  27806  opsqrlem1  27841  hst1h  27928  mdsl0  28011  superpos  28055  sumdmdlem  28119  cdj3lem1  28135  xrpxdivcld  28452  2sqn0  28455  xrge0npcan  28505  resvid2  28639  resvval2  28640  esumsnf  28933  esummulc1  28950  measxun2  29080  omsmeas  29203  omsmeasOLD  29204  sibfof  29221  probun  29300  bnj517  29744  mrsubfval  30194  msrval  30224  subdivcomb2  30409  dfrdg2  30490  bj-bary1lem1  31760  rdgeqoa  31817  finxpreclem2  31826  finxpreclem3  31829  poimirlem1  31985  poimirlem2  31986  poimirlem3  31987  poimirlem4  31988  poimirlem5  31989  poimirlem6  31990  poimirlem7  31991  poimirlem10  31994  poimirlem11  31995  poimirlem12  31996  poimirlem14  31998  poimirlem15  31999  poimirlem17  32001  poimirlem20  32004  poimirlem22  32006  poimirlem23  32007  poimirlem24  32008  poimirlem25  32009  poimirlem26  32010  poimirlem27  32011  mblfinlem2  32022  mblfinlem3  32023  ismblfin  32025  mbfposadd  32032  itg2addnclem  32037  itg2addnclem3  32039  itg2addnc  32040  ftc1anclem8  32068  areacirc  32081  ismtyval  32176  ismrer1  32214  rabeq12f  32444  csbeq12  32445  iuneq12f  32451  lsatcv1  32658  glbconN  32986  atltcvr  33044  3dim2  33077  islln2a  33126  2at0mat0  33134  islpln2a  33157  islvol2aN  33201  pmodlem2  33456  pmapjat1  33462  pcl0bN  33532  osumclN  33576  pexmidALTN  33587  lhp2at0nle  33644  4atexlemunv  33675  cdleme18b  33902  cdleme31sn1  33992  cdleme31sde  33996  cdleme31sn2  34000  ltrniotavalbN  34195  trljco  34351  cdlemh  34428  cdlemk40t  34529  cdlemk40f  34530  cdleml9  34595  dihmeetlem3N  34917  dochkrshp  34998  dihprrn  35038  dihjat1  35041  dvh3dim  35058  dochkrsm  35070  dochexmid  35080  lcfl7lem  35111  lcfl9a  35117  lclkrlem1  35118  mapdspex  35280  mapdindp2  35333  mapdh6dN  35351  hdmap1l6d  35426  hdmap11lem2  35457  hdmap14lem4a  35486  hdmapip0  35530  hlhilset  35549  bezoutr1  35880  jm2.26a  35899  radcnvrat  36706  sumsnd  37386  sumsnf  37685  icccncfext  37802  fperdvper  37827  dvcosax  37835  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem1OLD  37842  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  volioc  37886  itgiccshift  37894  stoweidlem34  37932  dirkercncflem2  38003  fourierdlem32  38039  fourierdlem41  38048  fourierdlem48  38055  fourierdlem64  38071  fourierdlem73  38080  fourierdlem79  38086  fourierdlem82  38089  fourierdlem97  38104  fourierdlem101  38108  fourierdlem109  38116  fourierdlem111  38118  fouriersw  38132  elaa2  38136  etransclem24  38160  etransclem25  38161  etransclem46  38182  ismeannd  38342  fzopredsuc  38757  mod2eq1n2dvds  38762  dfodd6  38804  dfeven4  38805  m1expevenALTV  38814  cplgr2vpr  39549  cplgr3v  39551  cusgrrusgr  39646  wlkOnwlk1l  39712  vdcusgra  39945  clintopval  40112  lmod0rng  40140  2zrngagrp  40215  rngcval  40236  ringcval  40282  dmmpt2ssx2  40390  zlmodzxzscm  40410  zlmodzxzadd  40411  domnmsuppn0  40426  rmsuppss  40427  scmsuppss  40429  ply1mulgsumlem4  40453  ldepsprlem  40537  lincresunit2  40543  m1modmmod  40596  nn0sumshdiglemB  40703
  Copyright terms: Public domain W3C validator