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

Theorem sylan9eqr 2434
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 2432 . 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  3134  csbied2  3230  onuninsuci  4753  fun2ssres  5427  fcoi1  5550  fcoi2  5551  funssfv  5679  fvtp1  5871  ot1stg  6293  ot2ndg  6294  mpt2mptsx  6346  dmmpt2ssx  6348  fmpt2x  6349  2ndconst  6368  mpt2xopoveq  6399  rdgeq12  6600  rdgsucmptnf  6616  frsucmptn  6625  abianfplem  6644  oev2  6696  oesuclem  6698  oawordeulem  6726  om00  6747  omass  6752  oeoa  6769  oeoe  6771  nnmass  6796  oaabs2  6817  omabs  6819  omxpenlem  7138  sbthlem4  7149  sbthlem6  7151  fodomr  7187  ssenen  7210  fi0  7353  cantnfp1  7563  cnfcomlem  7582  cardaleph  7896  cflim2  8069  axdc4lem  8261  fpwwe2lem12  8442  fpwwe2lem13  8443  rankcf  8578  inatsk  8579  ltrnq  8782  addclprlem1  8819  mulclprlem  8822  1idpr  8832  prlem936  8850  reclem3pr  8852  mulcmpblnrlem  8874  recexsrlem  8904  map2psrpr  8911  nnnn0addcl  10176  zindd  10296  qaddcl  10515  qmulcl  10517  qreccl  10519  xaddnemnf  10745  xaddnepnf  10746  xaddcom  10749  xnegdi  10752  xaddass  10753  xpncan  10755  xleadd1a  10757  xlt2add  10764  rexmul  10775  xmulgt0  10787  xmulge0  10788  xmulasslem3  10790  xlemul1a  10792  xadddilem  10798  xadddi2  10801  seqf1olem2  11283  expp1  11308  expneg  11309  expcllem  11312  mulexp  11339  expmul  11345  bcpasc  11532  fseq1hash  11570  hashinfxadd  11579  hashfzo  11614  hashf1lem1  11624  brfi1indlem  11634  wrdf  11653  ccatval1  11665  ccatval2  11666  swrdval  11684  splval  11700  s4dom  11786  shftfn  11808  reim0b  11844  cjexp  11875  sqeqd  11891  fsumser  12444  sumsn  12454  binomlem  12528  expcnv  12563  ef0lem  12601  dvdsnegb  12787  sadadd2lem2  12882  gcdabs  12953  coprmdvds  13022  mulgcddvds  13024  pcge0  13155  pcadd  13178  pcmpt2  13182  prmreclem4  13207  ramval  13296  ramcl  13317  ressid2  13437  ressval2  13438  frmdval  14716  mulgfval  14811  mulgnn0subcl  14823  mulgnn0z  14830  isga  14988  symgval  15014  odid  15096  gexid  15135  frgpuptinv  15323  frgpup2  15328  dprdsn  15514  isabvd  15828  issrng  15858  lvecinv  16105  lspdisj2  16119  lspfixed  16120  lspexch  16121  sralem  16169  srasca  16173  sravsca  16174  mplval  16412  opsrval  16455  znval  16732  isphl  16775  indistopon  16981  0ntr  17051  pnrmopn  17322  kgenval  17481  pt1hmeo  17752  fmval  17889  fmf  17891  istmd  18018  istgp  18021  tsmsval2  18073  isxmet2d  18259  xpsxmetlem  18310  xpsmet  18313  blfval  18314  tmsval  18394  isnlm  18575  nmoleub  18629  idnghm  18641  blssioo  18690  blcvx  18693  icccvx  18839  pcorevlem  18915  isclm  18953  caufval  19092  iscms  19160  mbfsup  19416  i1f1  19442  dvexp3  19722  rolle  19734  dvivth  19754  evl1fval  19807  deg1add  19886  0dgr  20024  coefv0  20026  elqaalem2  20097  dvradcnv  20197  abelthlem8  20215  efper  20247  logtayl  20411  abscxpbnd  20497  dcubic2  20544  rlimcnp2  20665  cvxcl  20683  vmaval  20756  chtub  20856  logexprlim  20869  dchrsum2  20912  sumdchr2  20914  bposlem2  20929  lgsdir  20974  lgsne0  20977  lgsdirnn0  20983  lgsdinn0  20984  lgsquadlem2  20999  dchrvmasum2if  21051  dchrvmasumiflem1  21055  rpvmasum2  21066  pntpbnd1  21140  ostth2lem4  21190  usgraedgprv  21256  vdgr1d  21515  vdgr1b  21516  vdgr1a  21518  eupatrl  21531  grpoidinvlem2  21634  grposn  21644  gxnn0neg  21692  gxid  21702  vcz  21890  nvz  21999  lnon0  22140  ipasslem2  22174  htthlem  22261  hvpncan  22382  hiidge0  22441  normgt0  22470  hsn0elch  22591  shsel3  22658  spansneleq  22913  normcan  22919  h1datomi  22924  fh1  22961  spansncvi  22995  5oalem1  22997  5oalem3  22999  5oalem5  23001  3oalem2  23006  pjdsi  23055  kbpj  23300  0hmop  23327  0lnfn  23329  adj0  23338  nlelshi  23404  branmfn  23449  opsqrlem1  23484  hst1h  23571  mdsl0  23654  superpos  23698  sumdmdlem  23762  cdj3lem1  23778  nvof1o  23876  xrpxdivcld  24013  xrge0npcan  24038  esumsn  24245  esummulc1  24260  measxun2  24351  probun  24449  zetacvg  24571  lgamgulmlem2  24586  subdivcomb2  24968  prodsn  25058  dfrdg2  25169  ax5seglem1  25574  ax5seglem2  25575  ax5seglem5  25579  bpolylem  25801  bpoly2  25810  bpoly3  25811  itg2addnclem  25950  areacirc  25981  ismtyval  26193  ismrer1  26231  bezoutr1  26735  jm2.26a  26755  f1omvdco2  27053  sumsnd  27358  stoweidlem34  27444  bnj517  28587  lsatcv1  29214  glbconN  29542  atltcvr  29600  3dim2  29633  islln2a  29682  2at0mat0  29690  islpln2a  29713  islvol2aN  29757  pmodlem2  30012  pmapjat1  30018  pcl0bN  30088  osumclN  30132  pexmidALTN  30143  lhp2at0nle  30200  4atexlemunv  30231  cdleme18b  30457  cdleme31sn1  30546  cdleme31sde  30550  cdleme31sn2  30554  ltrniotavalbN  30749  trljco  30905  cdlemh  30982  cdlemk40t  31083  cdlemk40f  31084  cdleml9  31149  dihmeetlem3N  31471  dochkrshp  31552  dihprrn  31592  dihjat1  31595  dvh3dim  31612  dochkrsm  31624  dochexmid  31634  lcfl7lem  31665  lcfl9a  31671  lclkrlem1  31672  mapdspex  31834  mapdindp2  31887  mapdh6dN  31905  hdmap1l6d  31980  hdmap11lem2  32011  hdmap14lem4a  32040  hdmapip0  32084  hlhilset  32103
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 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2373
  Copyright terms: Public domain W3C validator