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

Theorem sylan9eqr 2445
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 2443 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 451 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2374
This theorem is referenced by:  sbcied2  3290  csbied2  3376  fun2ssres  5537  fcoi1  5667  fcoi2  5668  funssfv  5789  fvtp1  6020  nvof1o  6087  onuninsuci  6574  ot1stg  6713  ot2ndg  6714  el2xptp0  6743  mpt2mptsx  6762  dmmpt2ssx  6764  fmpt2x  6765  2ndconst  6788  mpt2xopoveq  6865  rdgeq12  6997  rdgsucmptnf  7013  frsucmptn  7022  oev2  7091  oesuclem  7093  oawordeulem  7121  om00  7142  omass  7147  oeoa  7164  oeoe  7166  nnmass  7191  oaabs2  7212  omabs  7214  omxpenlem  7537  sbthlem4  7549  sbthlem6  7551  fodomr  7587  ssenen  7610  fi0  7795  cantnfp1  8013  cantnfp1OLD  8039  cnfcomlem  8056  cnfcomlemOLD  8064  cardaleph  8383  cflim2  8556  axdc4lem  8748  fpwwe2lem12  8930  fpwwe2lem13  8931  rankcf  9066  inatsk  9067  ltrnq  9268  addclprlem1  9305  mulclprlem  9308  1idpr  9318  prlem936  9336  reclem3pr  9338  mulcmpblnrlem  9358  recexsrlem  9391  map2psrpr  9398  nnnn0addcl  10743  zindd  10880  qaddcl  11117  qmulcl  11119  qreccl  11121  xaddnemnf  11354  xaddnepnf  11355  xaddcom  11358  xnegdi  11361  xaddass  11362  xpncan  11364  xleadd1a  11366  xlt2add  11373  rexmul  11384  xmulgt0  11396  xmulge0  11397  xmulasslem3  11399  xlemul1a  11401  xadddilem  11407  xadddi2  11410  modm1p1mod0  11941  seqf1olem2  12050  expp1  12076  expneg  12077  expcllem  12080  mulexp  12108  expmul  12114  bcpasc  12301  hashrabsn01  12344  fseq1hash  12347  hashinfxadd  12356  hashfzo  12391  ffzo0hash  12393  fz0hash  12403  hashf1lem1  12408  hashge2el2dif  12425  brfi1indlem  12435  lsw0  12494  ccatval1  12504  ccatval2  12505  swrdval  12553  reuccats1  12617  splval  12638  repswswrd  12667  2cshwcshw  12704  s4dom  12778  wrdlen2i  12795  shftfn  12908  reim0b  12954  cjexp  12985  sqeqd  13001  fsumser  13554  sumsn  13565  binomlem  13643  expcnv  13677  prodsn  13769  ef0lem  13816  dvdsnegb  14003  sadadd2lem2  14102  gcdabs  14173  coprmdvds  14245  mulgcddvds  14247  pcge0  14387  pcadd  14410  pcmpt2  14414  prmreclem4  14439  ramval  14528  ramcl  14549  ressid2  14689  ressval2  14690  mrcmndind  16114  frmdval  16136  mgm2nsgrplem3  16155  mulgfval  16260  mulgnn0subcl  16272  mulgnn0z  16279  isga  16446  symgval  16521  symgextfve  16561  symgfixf1  16579  f1omvdco2  16590  psgnsn  16662  odid  16679  gexid  16718  frgpuptinv  16906  frgpup2  16911  dprdsn  17196  srgmulgass  17295  srgpcomp  17296  srgbinomlem4  17307  f1rhm0to0  17502  f1rhm0to0ALT  17503  isabvd  17582  issrng  17612  lmodvsmmulgdi  17660  mptscmfsupp0  17689  lvecinv  17872  lspdisj2  17886  lspfixed  17887  lspexch  17888  sralem  17936  srasca  17940  sravsca  17941  sraip  17942  assamulgscmlem2  18111  mplval  18197  opsrval  18252  cply1mul  18448  gsummoncoe1  18459  evl1fval  18477  znval  18665  psgndiflemB  18727  isphl  18754  scmate  19097  scmatscm  19100  mdetdiagid  19187  mdetunilem7  19205  mdetuni0  19208  gsummatr01lem3  19244  gsummatr01lem4  19245  gsummatr01  19246  slesolinvbi  19268  cpmatacl  19302  cpmatinvcl  19303  pmatcollpw2lem  19363  monmatcollpw  19365  pmatcollpwfi  19368  mp2pm2mplem4  19395  pm2mp  19411  cpmadugsumlemF  19462  cpmadugsumfi  19463  cpmadumatpoly  19469  cayhamlem4  19474  cayleyhamilton0  19475  cayleyhamiltonALT  19477  indistopon  19587  0ntr  19658  pnrmopn  19930  reftr  20100  kgenval  20121  pt1hmeo  20392  fmval  20529  fmf  20531  istmd  20658  istgp  20661  tsmsval2  20713  isxmet2d  20915  xpsxmetlem  20967  xpsmet  20970  blfvalps  20971  tmsval  21069  isnlm  21269  nmoleub  21323  idnghm  21335  blssioo  21385  blcvx  21388  icccvx  21535  pcorevlem  21611  isclm  21649  caufval  21799  iscms  21869  mbfsup  22156  i1f1  22182  dvexp3  22464  rolle  22476  dvivth  22496  deg1add  22589  0dgr  22727  coefv0  22730  elqaalem2  22801  dvradcnv  22901  abelthlem8  22919  efper  22957  logtayl  23128  abscxpbnd  23214  relogbcxpb  23245  dcubic2  23291  rlimcnp2  23413  cvxcl  23431  vmaval  23504  chtub  23604  logexprlim  23617  dchrsum2  23660  sumdchr2  23662  bposlem2  23677  lgsdir  23722  lgsne0  23725  lgsdirnn0  23731  lgsdinn0  23732  lgsquadlem2  23747  dchrvmasum2if  23799  dchrvmasumiflem1  23803  rpvmasum2  23814  pntpbnd1  23888  ostth2lem4  23938  trgcgrg  24026  ax5seglem1  24352  ax5seglem2  24353  ax5seglem5  24357  usgraedgprv  24497  wwlknimp  24808  wwlknextbi  24846  wwlkextwrd  24849  clwlkisclwwlklem2fv1  24903  clwlkisclwwlklem2a4  24905  clwlkisclwwlklem0  24909  clwwlkf  24915  clwwlkf1  24917  wwlkext2clwwlk  24924  clwwisshclww  24928  erclwwlkeqlen  24933  eleclclwwlknlem2  24939  erclwwlkneqlen  24945  usghashecclwwlk  24956  vdgr1d  25024  vdgr1b  25025  vdgr1a  25027  cusgraisrusgra  25059  rusgra0edg  25076  eupatrl  25089  usg2spot2nb  25186  grpoidinvlem2  25324  grposn  25334  gxnn0neg  25382  gxid  25392  vcz  25580  nvz  25689  lnon0  25830  ipasslem2  25864  htthlem  25951  hvpncan  26073  hiidge0  26132  normgt0  26161  hsn0elch  26283  shsel3  26350  spansneleq  26605  normcan  26611  h1datomi  26616  fh1  26653  spansncvi  26687  5oalem1  26689  5oalem3  26691  5oalem5  26693  3oalem2  26698  pjdsi  26747  kbpj  26991  0hmop  27018  0lnfn  27020  adj0  27029  nlelshi  27095  branmfn  27140  opsqrlem1  27175  hst1h  27262  mdsl0  27345  superpos  27389  sumdmdlem  27453  cdj3lem1  27469  xrpxdivcld  27784  2sqn0  27787  xrge0npcan  27837  resvid2  27972  resvval2  27973  esumsnf  28212  esummulc1  28229  measxun2  28337  omsmeas  28450  sibfof  28465  probun  28541  zetacvg  28746  lgamgulmlem2  28761  mrsubfval  29057  msrval  29087  subdivcomb2  29272  dfrdg2  29393  wfrlem10  29517  bpolylem  29963  bpoly2  29972  bpoly3  29973  mblfinlem2  30217  mblfinlem3  30218  ismblfin  30220  mbfposadd  30227  itg2addnclem  30232  itg2addnclem3  30234  itg2addnc  30235  ftc1anclem8  30263  areacirc  30278  ismtyval  30462  ismrer1  30500  rabeq12f  30731  csbeq12  30732  iuneq12f  30738  bezoutr1  31089  jm2.26a  31108  radcnvrat  31363  dvdslcm  31372  lcmeq0  31374  lcmcl  31375  lcmabs  31379  lcmgcdlem  31380  lcmdvds  31382  sumsnd  31568  sumsnf  31736  prodsnf  31753  icccncfext  31856  fperdvper  31881  dvcosax  31889  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  volioc  31937  itgiccshift  31945  stoweidlem34  31982  dirkercncflem2  32052  fourierdlem32  32087  fourierdlem41  32096  fourierdlem48  32103  fourierdlem64  32119  fourierdlem73  32128  fourierdlem79  32134  fourierdlem82  32137  fourierdlem97  32152  fourierdlem101  32156  fourierdlem109  32164  fourierdlem111  32166  fouriersw  32180  etransclem24  32207  etransclem25  32208  etransclem46  32229  mod2eq1n2dvds  32462  dfodd6  32480  dfeven4  32481  m1expevenALTV  32490  vdcusgra  32677  clintopval  32846  lmod0rng  32874  2zrngagrp  32949  rngcval  32970  ringcval  33016  dmmpt2ssx2  33126  zlmodzxzscm  33146  zlmodzxzadd  33147  domnmsuppn0  33162  rmsuppss  33163  scmsuppss  33165  ply1mulgsumlem4  33189  ldepsprlem  33273  lincresunit2  33279  m1modmmod  33334  nn0sumshdiglemB  33441  bnj517  34290  bj-bary1lem1  35024  lsatcv1  35186  glbconN  35514  atltcvr  35572  3dim2  35605  islln2a  35654  2at0mat0  35662  islpln2a  35685  islvol2aN  35729  pmodlem2  35984  pmapjat1  35990  pcl0bN  36060  osumclN  36104  pexmidALTN  36115  lhp2at0nle  36172  4atexlemunv  36203  cdleme18b  36430  cdleme31sn1  36520  cdleme31sde  36524  cdleme31sn2  36528  ltrniotavalbN  36723  trljco  36879  cdlemh  36956  cdlemk40t  37057  cdlemk40f  37058  cdleml9  37123  dihmeetlem3N  37445  dochkrshp  37526  dihprrn  37566  dihjat1  37569  dvh3dim  37586  dochkrsm  37598  dochexmid  37608  lcfl7lem  37639  lcfl9a  37645  lclkrlem1  37646  mapdspex  37808  mapdindp2  37861  mapdh6dN  37879  hdmap1l6d  37954  hdmap11lem2  37985  hdmap14lem4a  38014  hdmapip0  38058  hlhilset  38077
  Copyright terms: Public domain W3C validator