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

Theorem sylan9eqr 2479
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 2477 . 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 1663  ax-4 1676  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2416
This theorem is referenced by:  sbcied2  3275  csbied2  3361  fun2ssres  5580  fcoi1  5712  fcoi2  5713  funssfv  5835  fvtp1  6065  nvof1o  6133  onuninsuci  6620  ot1stg  6760  ot2ndg  6761  el2xptp0  6790  mpt2mptsx  6809  dmmpt2ssx  6811  fmpt2x  6812  2ndconst  6835  mpt2xopoveq  6915  wfrlem10  6995  rdgeq12  7081  rdgsucmptnf  7097  frsucmptn  7106  oev2  7175  oesuclem  7177  oawordeulem  7205  om00  7226  omass  7231  oeoa  7248  oeoe  7250  nnmass  7275  oaabs2  7296  omabs  7298  omxpenlem  7621  sbthlem4  7633  sbthlem6  7635  fodomr  7671  ssenen  7694  fi0  7882  cantnfp1  8133  cnfcomlem  8151  cardaleph  8466  cflim2  8639  axdc4lem  8831  fpwwe2lem12  9012  fpwwe2lem13  9013  rankcf  9148  inatsk  9149  ltrnq  9350  addclprlem1  9387  mulclprlem  9390  1idpr  9400  prlem936  9418  reclem3pr  9420  mulcmpblnrlem  9440  recexsrlem  9473  map2psrpr  9480  nnnn0addcl  10846  zindd  10982  qaddcl  11226  qmulcl  11228  qreccl  11230  xaddnemnf  11473  xaddnepnf  11474  xaddcom  11477  xnegdi  11480  xaddass  11481  xpncan  11483  xleadd1a  11485  xlt2add  11492  rexmul  11503  xmulgt0  11515  xmulge0  11516  xmulasslem3  11518  xlemul1a  11520  xadddilem  11526  xadddi2  11529  modm1p1mod0  12086  seqf1olem2  12198  expp1  12224  expneg  12225  expcllem  12228  mulexp  12256  expmul  12262  bcpasc  12451  hashrabsn01  12497  fseq1hash  12500  hashinfxadd  12509  hashfzo  12544  ffzo0hash  12546  fz0hash  12556  hashf1lem1  12561  hashge2el2dif  12580  brfi1indlem  12592  lsw0  12655  ccatval1  12665  ccatval2  12666  swrdval  12714  reuccats1  12778  splval  12799  repswswrd  12828  2cshwcshw  12865  s4dom  12943  wrdlen2i  12960  shftfn  13075  reim0b  13121  cjexp  13152  sqeqd  13168  fsumser  13734  sumsn  13745  binomlem  13825  expcnv  13860  prodsn  13954  prodsnf  13956  bpolylem  14039  bpoly2  14048  bpoly3  14049  ef0lem  14071  dvdsnegb  14258  sadadd2lem2  14362  gcdabs  14435  dvdslcm  14501  lcmeq0  14503  lcmcl  14504  lcmabs  14508  lcmgcdlem  14509  lcmdvds  14511  lcmf0val  14530  lcmftp  14547  lcmfunsnlem2  14551  coprmdvds  14597  mulgcddvds  14599  pcge0  14749  pcadd  14772  pcmpt2  14776  prmreclem4  14801  ramval  14898  ramvalOLD  14899  ramcl  14925  fvprmselelfz  14940  fvprmselgcd1  14941  prmdvdsprmorOLD  14953  ressid2  15115  ressval2  15116  mrcmndind  16551  frmdval  16573  mgm2nsgrplem3  16592  mulgfval  16697  mulgnn0subcl  16709  mulgnn0z  16716  isga  16883  symgval  16958  symgextfve  16998  symgfixf1  17016  f1omvdco2  17027  psgnsn  17099  odid  17125  odidOLD  17141  gexid  17170  frgpuptinv  17359  frgpup2  17364  dprdsn  17607  srgmulgass  17702  srgpcomp  17703  srgbinomlem4  17714  f1rhm0to0  17906  f1rhm0to0ALT  17907  isabvd  17986  issrng  18016  lmodvsmmulgdi  18064  mptscmfsupp0  18091  lvecinv  18274  lspdisj2  18288  lspfixed  18289  lspexch  18290  sralem  18338  srasca  18342  sravsca  18343  sraip  18344  assamulgscmlem2  18511  mplval  18590  opsrval  18636  cply1mul  18825  gsummoncoe1  18836  evl1fval  18854  znval  19043  psgndiflemB  19105  isphl  19132  scmate  19472  scmatscm  19475  mdetdiagid  19562  mdetunilem7  19580  mdetuni0  19583  gsummatr01lem3  19619  gsummatr01lem4  19620  gsummatr01  19621  slesolinvbi  19643  cpmatacl  19677  cpmatinvcl  19678  pmatcollpw2lem  19738  monmatcollpw  19740  pmatcollpwfi  19743  mp2pm2mplem4  19770  pm2mp  19786  cpmadugsumlemF  19837  cpmadugsumfi  19838  cpmadumatpoly  19844  cayhamlem4  19849  cayleyhamilton0  19850  cayleyhamiltonALT  19852  indistopon  19953  0ntr  20024  pnrmopn  20296  reftr  20466  kgenval  20487  pt1hmeo  20758  fmval  20895  fmf  20897  istmd  21026  istgp  21029  tsmsval2  21081  isxmet2d  21279  xpsxmetlem  21331  xpsmet  21334  blfvalps  21335  tmsval  21433  isnlm  21615  nmoleub  21673  nmoleubOLD  21689  idnghm  21701  blssioo  21750  blcvx  21753  icccvx  21915  pcorevlem  21994  isclm  22032  caufval  22182  iscms  22250  mbfsup  22557  i1f1  22585  dvexp3  22867  rolle  22879  dvivth  22899  deg1add  22989  0dgr  23136  coefv0  23139  elqaalem2  23210  elqaalem2OLD  23213  dvradcnv  23313  abelthlem8  23331  efper  23371  logtayl  23542  abscxpbnd  23630  relogbcxpb  23661  dcubic2  23707  rlimcnp2  23829  cvxcl  23847  zetacvg  23877  lgamgulmlem2  23892  vmaval  23977  chtub  24077  logexprlim  24090  dchrsum2  24133  sumdchr2  24135  bposlem2  24150  lgsdir  24195  lgsne0  24198  lgsdirnn0  24204  lgsdinn0  24205  lgsquadlem2  24220  dchrvmasum2if  24272  dchrvmasumiflem1  24276  rpvmasum2  24287  pntpbnd1  24361  ostth2lem4  24411  trgcgrg  24497  ax5seglem1  24895  ax5seglem2  24896  ax5seglem5  24900  usgraedgprv  25040  wwlknimp  25352  wwlknextbi  25390  wwlkextwrd  25393  clwlkisclwwlklem2fv1  25447  clwlkisclwwlklem2a4  25449  clwlkisclwwlklem0  25453  clwwlkf  25459  clwwlkf1  25461  wwlkext2clwwlk  25468  clwwisshclww  25472  erclwwlkeqlen  25477  eleclclwwlknlem2  25483  erclwwlkneqlen  25489  usghashecclwwlk  25500  vdgr1d  25568  vdgr1b  25569  vdgr1a  25571  cusgraisrusgra  25603  rusgra0edg  25620  eupatrl  25633  usg2spot2nb  25730  grpoidinvlem2  25870  grposn  25880  gxnn0neg  25928  gxid  25938  vcz  26126  nvz  26235  lnon0  26376  ipasslem2  26410  htthlem  26507  hvpncan  26629  hiidge0  26688  normgt0  26717  hsn0elch  26838  shsel3  26905  spansneleq  27160  normcan  27166  h1datomi  27171  fh1  27208  spansncvi  27242  5oalem1  27244  5oalem3  27246  5oalem5  27248  3oalem2  27253  pjdsi  27302  kbpj  27546  0hmop  27573  0lnfn  27575  adj0  27584  nlelshi  27650  branmfn  27695  opsqrlem1  27730  hst1h  27817  mdsl0  27900  superpos  27944  sumdmdlem  28008  cdj3lem1  28024  xrpxdivcld  28350  2sqn0  28353  xrge0npcan  28403  resvid2  28538  resvval2  28539  esumsnf  28832  esummulc1  28849  measxun2  28979  omsmeas  29102  omsmeasOLD  29103  sibfof  29120  probun  29199  bnj517  29643  mrsubfval  30093  msrval  30123  subdivcomb2  30307  dfrdg2  30388  bj-bary1lem1  31623  rdgeqoa  31680  finxpreclem2  31689  finxpreclem3  31692  poimirlem1  31848  poimirlem2  31849  poimirlem3  31850  poimirlem4  31851  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem14  31861  poimirlem15  31862  poimirlem17  31864  poimirlem20  31867  poimirlem22  31869  poimirlem23  31870  poimirlem24  31871  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  mblfinlem2  31885  mblfinlem3  31886  ismblfin  31888  mbfposadd  31895  itg2addnclem  31900  itg2addnclem3  31902  itg2addnc  31903  ftc1anclem8  31931  areacirc  31944  ismtyval  32039  ismrer1  32077  rabeq12f  32307  csbeq12  32308  iuneq12f  32314  lsatcv1  32526  glbconN  32854  atltcvr  32912  3dim2  32945  islln2a  32994  2at0mat0  33002  islpln2a  33025  islvol2aN  33069  pmodlem2  33324  pmapjat1  33330  pcl0bN  33400  osumclN  33444  pexmidALTN  33455  lhp2at0nle  33512  4atexlemunv  33543  cdleme18b  33770  cdleme31sn1  33860  cdleme31sde  33864  cdleme31sn2  33868  ltrniotavalbN  34063  trljco  34219  cdlemh  34296  cdlemk40t  34397  cdlemk40f  34398  cdleml9  34463  dihmeetlem3N  34785  dochkrshp  34866  dihprrn  34906  dihjat1  34909  dvh3dim  34926  dochkrsm  34938  dochexmid  34948  lcfl7lem  34979  lcfl9a  34985  lclkrlem1  34986  mapdspex  35148  mapdindp2  35201  mapdh6dN  35219  hdmap1l6d  35294  hdmap11lem2  35325  hdmap14lem4a  35354  hdmapip0  35398  hlhilset  35417  bezoutr1  35749  jm2.26a  35768  radcnvrat  36576  sumsnd  37263  sumsnf  37532  icccncfext  37648  fperdvper  37673  dvcosax  37681  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem1OLD  37688  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  volioc  37732  itgiccshift  37740  stoweidlem34  37778  dirkercncflem2  37849  fourierdlem32  37885  fourierdlem41  37894  fourierdlem48  37901  fourierdlem64  37917  fourierdlem73  37926  fourierdlem79  37932  fourierdlem82  37935  fourierdlem97  37950  fourierdlem101  37954  fourierdlem109  37962  fourierdlem111  37964  fouriersw  37978  elaa2  37982  etransclem24  38006  etransclem25  38007  etransclem46  38028  ismeannd  38156  fzopredsuc  38533  mod2eq1n2dvds  38538  dfodd6  38580  dfeven4  38581  m1expevenALTV  38590  cplgr2vpr  39228  cplgr3v  39230  vdcusgra  39264  clintopval  39431  lmod0rng  39459  2zrngagrp  39534  rngcval  39555  ringcval  39601  dmmpt2ssx2  39711  zlmodzxzscm  39731  zlmodzxzadd  39732  domnmsuppn0  39747  rmsuppss  39748  scmsuppss  39750  ply1mulgsumlem4  39774  ldepsprlem  39858  lincresunit2  39864  m1modmmod  39917  nn0sumshdiglemB  40024
  Copyright terms: Public domain W3C validator