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

Theorem sylan9eqr 2530
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 2528 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 453 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459
This theorem is referenced by:  sbcied2  3369  csbied2  3463  fun2ssres  5629  fcoi1  5759  fcoi2  5760  funssfv  5881  fvtp1  6108  nvof1o  6174  onuninsuci  6659  ot1stg  6798  ot2ndg  6799  el2xptp0  6828  mpt2mptsx  6847  dmmpt2ssx  6849  fmpt2x  6850  2ndconst  6872  mpt2xopoveq  6947  rdgeq12  7079  rdgsucmptnf  7095  frsucmptn  7104  oev2  7173  oesuclem  7175  oawordeulem  7203  om00  7224  omass  7229  oeoa  7246  oeoe  7248  nnmass  7273  oaabs2  7294  omabs  7296  omxpenlem  7618  sbthlem4  7630  sbthlem6  7632  fodomr  7668  ssenen  7691  fi0  7880  cantnfp1  8100  cantnfp1OLD  8126  cnfcomlem  8143  cnfcomlemOLD  8151  cardaleph  8470  cflim2  8643  axdc4lem  8835  fpwwe2lem12  9019  fpwwe2lem13  9020  rankcf  9155  inatsk  9156  ltrnq  9357  addclprlem1  9394  mulclprlem  9397  1idpr  9407  prlem936  9425  reclem3pr  9427  mulcmpblnrlem  9447  recexsrlem  9480  map2psrpr  9487  nnnn0addcl  10826  zindd  10962  qaddcl  11198  qmulcl  11200  qreccl  11202  xaddnemnf  11433  xaddnepnf  11434  xaddcom  11437  xnegdi  11440  xaddass  11441  xpncan  11443  xleadd1a  11445  xlt2add  11452  rexmul  11463  xmulgt0  11475  xmulge0  11476  xmulasslem3  11478  xlemul1a  11480  xadddilem  11486  xadddi2  11489  modm1p1mod0  12006  seqf1olem2  12115  expp1  12141  expneg  12142  expcllem  12145  mulexp  12173  expmul  12179  bcpasc  12367  hashrabsn01  12409  fseq1hash  12412  hashinfxadd  12421  hashfzo  12452  ffzohash  12454  fseq0hash  12456  fz0hash  12465  hashf1lem1  12470  hashge2el2dif  12487  brfi1indlem  12497  wrdf  12519  lsw0  12551  ccatval1  12560  ccatval2  12561  ccatw2s1p1  12603  ccatw2s1p2  12604  swrdval  12607  reuccats1  12669  splval  12690  repswswrd  12719  2cshwcshw  12756  s4dom  12830  wrdlen2i  12847  shftfn  12869  reim0b  12915  cjexp  12946  sqeqd  12962  fsumser  13515  sumsn  13526  binomlem  13604  expcnv  13638  ef0lem  13676  dvdsnegb  13862  sadadd2lem2  13959  gcdabs  14030  coprmdvds  14102  mulgcddvds  14104  pcge0  14244  pcadd  14267  pcmpt2  14271  prmreclem4  14296  ramval  14385  ramcl  14406  ressid2  14543  ressval2  14544  mrcmndind  15816  frmdval  15851  mulgfval  15953  mulgnn0subcl  15965  mulgnn0z  15972  isga  16134  symgval  16209  symgextfve  16249  symgfixf1  16268  f1omvdco2  16279  psgnsn  16351  odid  16368  gexid  16407  frgpuptinv  16595  frgpup2  16600  dprdsn  16885  srgmulgass  16984  srgpcomp  16985  srgbinomlem4  16996  f1rhm0to0  17189  f1rhm0to0ALT  17190  isabvd  17269  issrng  17299  lmodvsmmulgdi  17347  mptscmfsupp0  17376  lvecinv  17559  lspdisj2  17573  lspfixed  17574  lspexch  17575  sralem  17623  srasca  17627  sravsca  17628  sraip  17629  assamulgscmlem2  17797  mplval  17883  opsrval  17938  cply1mul  18134  gsummoncoe1  18145  evl1fval  18163  znval  18367  psgndiflemB  18431  isphl  18458  scmate  18807  scmatscm  18810  mdetdiagid  18897  mdetunilem7  18915  mdetuni0  18918  gsummatr01lem3  18954  gsummatr01lem4  18955  gsummatr01  18956  slesolinvbi  18978  cpmatacl  19012  cpmatinvcl  19013  pmatcollpw2lem  19073  monmatcollpw  19075  pmatcollpwfi  19078  mp2pm2mplem4  19105  pm2mp  19121  cpmadugsumlemF  19172  cpmadugsumfi  19173  cpmadumatpoly  19179  cayhamlem4  19184  cayleyhamilton0  19185  cayleyhamiltonALT  19187  indistopon  19296  0ntr  19366  pnrmopn  19638  kgenval  19799  pt1hmeo  20070  fmval  20207  fmf  20209  istmd  20336  istgp  20339  tsmsval2  20391  isxmet2d  20593  xpsxmetlem  20645  xpsmet  20648  blfvalps  20649  tmsval  20747  isnlm  20947  nmoleub  21001  idnghm  21013  blssioo  21063  blcvx  21066  icccvx  21213  pcorevlem  21289  isclm  21327  caufval  21477  iscms  21547  mbfsup  21834  i1f1  21860  dvexp3  22142  rolle  22154  dvivth  22174  deg1add  22267  0dgr  22405  coefv0  22407  elqaalem2  22478  dvradcnv  22578  abelthlem8  22596  efper  22633  logtayl  22797  abscxpbnd  22883  dcubic2  22931  rlimcnp2  23052  cvxcl  23070  vmaval  23143  chtub  23243  logexprlim  23256  dchrsum2  23299  sumdchr2  23301  bposlem2  23316  lgsdir  23361  lgsne0  23364  lgsdirnn0  23370  lgsdinn0  23371  lgsquadlem2  23386  dchrvmasum2if  23438  dchrvmasumiflem1  23442  rpvmasum2  23453  pntpbnd1  23527  ostth2lem4  23577  ax5seglem1  23935  ax5seglem2  23936  ax5seglem5  23940  usgraedgprv  24080  wwlknimp  24391  wwlknextbi  24429  wwlkextwrd  24432  clwlkisclwwlklem2fv1  24486  clwlkisclwwlklem2a4  24488  clwlkisclwwlklem0  24492  clwwlkf  24498  clwwlkf1  24500  wwlkext2clwwlk  24507  clwwisshclww  24511  erclwwlkeqlen  24516  eleclclwwlknlem2  24522  erclwwlkneqlen  24528  usghashecclwwlk  24539  vdgr1d  24607  vdgr1b  24608  vdgr1a  24610  cusgraisrusgra  24642  rusgra0edg  24659  eupatrl  24672  usg2spot2nb  24770  grpoidinvlem2  24911  grposn  24921  gxnn0neg  24969  gxid  24979  vcz  25167  nvz  25276  lnon0  25417  ipasslem2  25451  htthlem  25538  hvpncan  25660  hiidge0  25719  normgt0  25748  hsn0elch  25870  shsel3  25937  spansneleq  26192  normcan  26198  h1datomi  26203  fh1  26240  spansncvi  26274  5oalem1  26276  5oalem3  26278  5oalem5  26280  3oalem2  26285  pjdsi  26334  kbpj  26579  0hmop  26606  0lnfn  26608  adj0  26617  nlelshi  26683  branmfn  26728  opsqrlem1  26763  hst1h  26850  mdsl0  26933  superpos  26977  sumdmdlem  27041  cdj3lem1  27057  xrpxdivcld  27327  xrge0npcan  27374  resvid2  27509  resvval2  27510  esumsn  27740  esummulc1  27755  measxun2  27849  probun  28026  zetacvg  28225  lgamgulmlem2  28240  subdivcomb2  28609  prodsn  28697  dfrdg2  28833  wfrlem10  28957  bpolylem  29415  bpoly2  29424  bpoly3  29425  mblfinlem2  29657  mblfinlem3  29658  ismblfin  29660  mbfposadd  29667  itg2addnclem  29671  itg2addnclem3  29673  itg2addnc  29674  ftc1anclem8  29702  areacirc  29717  ismtyval  29927  ismrer1  29965  rabeq12f  30197  csbeq12  30198  iuneq12f  30204  bezoutr1  30556  jm2.26a  30574  dvdslcm  30832  lcmeq0  30834  lcmcl  30835  lcmabs  30839  lcmgcdlem  30840  lcmdvds  30842  sumsnd  31007  icccncfext  31254  stoweidlem34  31362  fourierdlem73  31508  vdcusgra  31854  clintopval  31984  dmmpt2ssx2  32022  zlmodzxzscm  32042  zlmodzxzadd  32043  lmod0rng  32058  domnmsuppn0  32061  rmsuppss  32062  scmsuppss  32064  ply1mulgsumlem4  32088  ldepsprlem  32172  lincresunit2  32178  bnj517  33040  bj-bary1lem1  33770  lsatcv1  33863  glbconN  34191  atltcvr  34249  3dim2  34282  islln2a  34331  2at0mat0  34339  islpln2a  34362  islvol2aN  34406  pmodlem2  34661  pmapjat1  34667  pcl0bN  34737  osumclN  34781  pexmidALTN  34792  lhp2at0nle  34849  4atexlemunv  34880  cdleme18b  35106  cdleme31sn1  35195  cdleme31sde  35199  cdleme31sn2  35203  ltrniotavalbN  35398  trljco  35554  cdlemh  35631  cdlemk40t  35732  cdlemk40f  35733  cdleml9  35798  dihmeetlem3N  36120  dochkrshp  36201  dihprrn  36241  dihjat1  36244  dvh3dim  36261  dochkrsm  36273  dochexmid  36283  lcfl7lem  36314  lcfl9a  36320  lclkrlem1  36321  mapdspex  36483  mapdindp2  36536  mapdh6dN  36554  hdmap1l6d  36629  hdmap11lem2  36660  hdmap14lem4a  36689  hdmapip0  36733  hlhilset  36752
  Copyright terms: Public domain W3C validator