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

Theorem sylan9eqr 2458
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 2456 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 440 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649
This theorem is referenced by:  sbcied2  3158  csbied2  3254  onuninsuci  4779  fun2ssres  5453  fcoi1  5576  fcoi2  5577  funssfv  5705  fvtp1  5898  ot1stg  6320  ot2ndg  6321  mpt2mptsx  6373  dmmpt2ssx  6375  fmpt2x  6376  2ndconst  6395  mpt2xopoveq  6429  rdgeq12  6630  rdgsucmptnf  6646  frsucmptn  6655  abianfplem  6674  oev2  6726  oesuclem  6728  oawordeulem  6756  om00  6777  omass  6782  oeoa  6799  oeoe  6801  nnmass  6826  oaabs2  6847  omabs  6849  omxpenlem  7168  sbthlem4  7179  sbthlem6  7181  fodomr  7217  ssenen  7240  fi0  7383  cantnfp1  7593  cnfcomlem  7612  cardaleph  7926  cflim2  8099  axdc4lem  8291  fpwwe2lem12  8472  fpwwe2lem13  8473  rankcf  8608  inatsk  8609  ltrnq  8812  addclprlem1  8849  mulclprlem  8852  1idpr  8862  prlem936  8880  reclem3pr  8882  mulcmpblnrlem  8904  recexsrlem  8934  map2psrpr  8941  nnnn0addcl  10207  zindd  10327  qaddcl  10546  qmulcl  10548  qreccl  10550  xaddnemnf  10776  xaddnepnf  10777  xaddcom  10780  xnegdi  10783  xaddass  10784  xpncan  10786  xleadd1a  10788  xlt2add  10795  rexmul  10806  xmulgt0  10818  xmulge0  10819  xmulasslem3  10821  xlemul1a  10823  xadddilem  10829  xadddi2  10832  seqf1olem2  11318  expp1  11343  expneg  11344  expcllem  11347  mulexp  11374  expmul  11380  bcpasc  11567  fseq1hash  11605  hashinfxadd  11614  hashfzo  11649  hashf1lem1  11659  brfi1indlem  11669  wrdf  11688  ccatval1  11700  ccatval2  11701  swrdval  11719  splval  11735  s4dom  11821  shftfn  11843  reim0b  11879  cjexp  11910  sqeqd  11926  fsumser  12479  sumsn  12489  binomlem  12563  expcnv  12598  ef0lem  12636  dvdsnegb  12822  sadadd2lem2  12917  gcdabs  12988  coprmdvds  13057  mulgcddvds  13059  pcge0  13190  pcadd  13213  pcmpt2  13217  prmreclem4  13242  ramval  13331  ramcl  13352  ressid2  13472  ressval2  13473  frmdval  14751  mulgfval  14846  mulgnn0subcl  14858  mulgnn0z  14865  isga  15023  symgval  15049  odid  15131  gexid  15170  frgpuptinv  15358  frgpup2  15363  dprdsn  15549  isabvd  15863  issrng  15893  lvecinv  16140  lspdisj2  16154  lspfixed  16155  lspexch  16156  sralem  16204  srasca  16208  sravsca  16209  mplval  16447  opsrval  16490  znval  16771  isphl  16814  indistopon  17020  0ntr  17090  pnrmopn  17361  kgenval  17520  pt1hmeo  17791  fmval  17928  fmf  17930  istmd  18057  istgp  18060  tsmsval2  18112  isxmet2d  18310  xpsxmetlem  18362  xpsmet  18365  blfvalps  18366  tmsval  18464  isnlm  18664  nmoleub  18718  idnghm  18730  blssioo  18779  blcvx  18782  icccvx  18928  pcorevlem  19004  isclm  19042  caufval  19181  iscms  19251  mbfsup  19509  i1f1  19535  dvexp3  19815  rolle  19827  dvivth  19847  evl1fval  19900  deg1add  19979  0dgr  20117  coefv0  20119  elqaalem2  20190  dvradcnv  20290  abelthlem8  20308  efper  20340  logtayl  20504  abscxpbnd  20590  dcubic2  20637  rlimcnp2  20758  cvxcl  20776  vmaval  20849  chtub  20949  logexprlim  20962  dchrsum2  21005  sumdchr2  21007  bposlem2  21022  lgsdir  21067  lgsne0  21070  lgsdirnn0  21076  lgsdinn0  21077  lgsquadlem2  21092  dchrvmasum2if  21144  dchrvmasumiflem1  21148  rpvmasum2  21159  pntpbnd1  21233  ostth2lem4  21283  usgraedgprv  21349  vdgr1d  21627  vdgr1b  21628  vdgr1a  21630  eupatrl  21643  grpoidinvlem2  21746  grposn  21756  gxnn0neg  21804  gxid  21814  vcz  22002  nvz  22111  lnon0  22252  ipasslem2  22286  htthlem  22373  hvpncan  22494  hiidge0  22553  normgt0  22582  hsn0elch  22703  shsel3  22770  spansneleq  23025  normcan  23031  h1datomi  23036  fh1  23073  spansncvi  23107  5oalem1  23109  5oalem3  23111  5oalem5  23113  3oalem2  23118  pjdsi  23167  kbpj  23412  0hmop  23439  0lnfn  23441  adj0  23450  nlelshi  23516  branmfn  23561  opsqrlem1  23596  hst1h  23683  mdsl0  23766  superpos  23810  sumdmdlem  23874  cdj3lem1  23890  nvof1o  23993  xrpxdivcld  24134  xrge0npcan  24169  esumsn  24409  esummulc1  24424  measxun2  24517  probun  24630  zetacvg  24752  lgamgulmlem2  24767  subdivcomb2  25149  prodsn  25239  binomfallfaclem2  25307  dfrdg2  25366  ax5seglem1  25771  ax5seglem2  25772  ax5seglem5  25776  bpolylem  25998  bpoly2  26007  bpoly3  26008  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  mbfposadd  26153  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  areacirc  26187  ismtyval  26399  ismrer1  26437  bezoutr1  26941  jm2.26a  26961  f1omvdco2  27259  sumsnd  27564  stoweidlem34  27650  el2xptp0  27949  fseq0hash  27993  swrdccat3b  28031  usg2spot2nb  28168  bnj517  28962  lsatcv1  29531  glbconN  29859  atltcvr  29917  3dim2  29950  islln2a  29999  2at0mat0  30007  islpln2a  30030  islvol2aN  30074  pmodlem2  30329  pmapjat1  30335  pcl0bN  30405  osumclN  30449  pexmidALTN  30460  lhp2at0nle  30517  4atexlemunv  30548  cdleme18b  30774  cdleme31sn1  30863  cdleme31sde  30867  cdleme31sn2  30871  ltrniotavalbN  31066  trljco  31222  cdlemh  31299  cdlemk40t  31400  cdlemk40f  31401  cdleml9  31466  dihmeetlem3N  31788  dochkrshp  31869  dihprrn  31909  dihjat1  31912  dvh3dim  31929  dochkrsm  31941  dochexmid  31951  lcfl7lem  31982  lcfl9a  31988  lclkrlem1  31989  mapdspex  32151  mapdindp2  32204  mapdh6dN  32222  hdmap1l6d  32297  hdmap11lem2  32328  hdmap14lem4a  32357  hdmapip0  32401  hlhilset  32420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator