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

Theorem sylan9eqr 2489
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 2487 . 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 1652
This theorem is referenced by:  sbcied2  3190  csbied2  3286  onuninsuci  4812  fun2ssres  5486  fcoi1  5609  fcoi2  5610  funssfv  5738  fvtp1  5931  ot1stg  6353  ot2ndg  6354  mpt2mptsx  6406  dmmpt2ssx  6408  fmpt2x  6409  2ndconst  6428  mpt2xopoveq  6462  rdgeq12  6663  rdgsucmptnf  6679  frsucmptn  6688  abianfplem  6707  oev2  6759  oesuclem  6761  oawordeulem  6789  om00  6810  omass  6815  oeoa  6832  oeoe  6834  nnmass  6859  oaabs2  6880  omabs  6882  omxpenlem  7201  sbthlem4  7212  sbthlem6  7214  fodomr  7250  ssenen  7273  fi0  7417  cantnfp1  7629  cnfcomlem  7648  cardaleph  7962  cflim2  8135  axdc4lem  8327  fpwwe2lem12  8508  fpwwe2lem13  8509  rankcf  8644  inatsk  8645  ltrnq  8848  addclprlem1  8885  mulclprlem  8888  1idpr  8898  prlem936  8916  reclem3pr  8918  mulcmpblnrlem  8940  recexsrlem  8970  map2psrpr  8977  nnnn0addcl  10243  zindd  10363  qaddcl  10582  qmulcl  10584  qreccl  10586  xaddnemnf  10812  xaddnepnf  10813  xaddcom  10816  xnegdi  10819  xaddass  10820  xpncan  10822  xleadd1a  10824  xlt2add  10831  rexmul  10842  xmulgt0  10854  xmulge0  10855  xmulasslem3  10857  xlemul1a  10859  xadddilem  10865  xadddi2  10868  seqf1olem2  11355  expp1  11380  expneg  11381  expcllem  11384  mulexp  11411  expmul  11417  bcpasc  11604  fseq1hash  11642  hashinfxadd  11651  hashfzo  11686  hashf1lem1  11696  brfi1indlem  11706  wrdf  11725  ccatval1  11737  ccatval2  11738  swrdval  11756  splval  11772  s4dom  11858  shftfn  11880  reim0b  11916  cjexp  11947  sqeqd  11963  fsumser  12516  sumsn  12526  binomlem  12600  expcnv  12635  ef0lem  12673  dvdsnegb  12859  sadadd2lem2  12954  gcdabs  13025  coprmdvds  13094  mulgcddvds  13096  pcge0  13227  pcadd  13250  pcmpt2  13254  prmreclem4  13279  ramval  13368  ramcl  13389  ressid2  13509  ressval2  13510  frmdval  14788  mulgfval  14883  mulgnn0subcl  14895  mulgnn0z  14902  isga  15060  symgval  15086  odid  15168  gexid  15207  frgpuptinv  15395  frgpup2  15400  dprdsn  15586  isabvd  15900  issrng  15930  lvecinv  16177  lspdisj2  16191  lspfixed  16192  lspexch  16193  sralem  16241  srasca  16245  sravsca  16246  mplval  16484  opsrval  16527  znval  16808  isphl  16851  indistopon  17057  0ntr  17127  pnrmopn  17399  kgenval  17559  pt1hmeo  17830  fmval  17967  fmf  17969  istmd  18096  istgp  18099  tsmsval2  18151  isxmet2d  18349  xpsxmetlem  18401  xpsmet  18404  blfvalps  18405  tmsval  18503  isnlm  18703  nmoleub  18757  idnghm  18769  blssioo  18818  blcvx  18821  icccvx  18967  pcorevlem  19043  isclm  19081  caufval  19220  iscms  19290  mbfsup  19548  i1f1  19574  dvexp3  19854  rolle  19866  dvivth  19886  evl1fval  19939  deg1add  20018  0dgr  20156  coefv0  20158  elqaalem2  20229  dvradcnv  20329  abelthlem8  20347  efper  20379  logtayl  20543  abscxpbnd  20629  dcubic2  20676  rlimcnp2  20797  cvxcl  20815  vmaval  20888  chtub  20988  logexprlim  21001  dchrsum2  21044  sumdchr2  21046  bposlem2  21061  lgsdir  21106  lgsne0  21109  lgsdirnn0  21115  lgsdinn0  21116  lgsquadlem2  21131  dchrvmasum2if  21183  dchrvmasumiflem1  21187  rpvmasum2  21198  pntpbnd1  21272  ostth2lem4  21322  usgraedgprv  21388  vdgr1d  21666  vdgr1b  21667  vdgr1a  21669  eupatrl  21682  grpoidinvlem2  21785  grposn  21795  gxnn0neg  21843  gxid  21853  vcz  22041  nvz  22150  lnon0  22291  ipasslem2  22325  htthlem  22412  hvpncan  22533  hiidge0  22592  normgt0  22621  hsn0elch  22742  shsel3  22809  spansneleq  23064  normcan  23070  h1datomi  23075  fh1  23112  spansncvi  23146  5oalem1  23148  5oalem3  23150  5oalem5  23152  3oalem2  23157  pjdsi  23206  kbpj  23451  0hmop  23478  0lnfn  23480  adj0  23489  nlelshi  23555  branmfn  23600  opsqrlem1  23635  hst1h  23722  mdsl0  23805  superpos  23849  sumdmdlem  23913  cdj3lem1  23929  nvof1o  24032  xrpxdivcld  24173  xrge0npcan  24208  esumsn  24448  esummulc1  24463  measxun2  24556  probun  24669  zetacvg  24791  lgamgulmlem2  24806  subdivcomb2  25188  prodsn  25278  dfrdg2  25415  wfrlem10  25539  ax5seglem1  25859  ax5seglem2  25860  ax5seglem5  25864  bpolylem  26086  bpoly2  26095  bpoly3  26096  mblfinlem  26234  mblfinlem2  26235  ismblfin  26237  mbfposadd  26244  itg2addnclem  26246  itg2addnclem3  26248  itg2addnc  26249  ftc1anclem2  26271  ftc1anclem8  26277  areacirc  26288  ismtyval  26500  ismrer1  26538  bezoutr1  27042  jm2.26a  27062  f1omvdco2  27359  sumsnd  27664  stoweidlem34  27750  el2xptp0  28051  fseq0hash  28116  lswrd0  28227  usg2spot2nb  28391  bnj517  29193  lsatcv1  29783  glbconN  30111  atltcvr  30169  3dim2  30202  islln2a  30251  2at0mat0  30259  islpln2a  30282  islvol2aN  30326  pmodlem2  30581  pmapjat1  30587  pcl0bN  30657  osumclN  30701  pexmidALTN  30712  lhp2at0nle  30769  4atexlemunv  30800  cdleme18b  31026  cdleme31sn1  31115  cdleme31sde  31119  cdleme31sn2  31123  ltrniotavalbN  31318  trljco  31474  cdlemh  31551  cdlemk40t  31652  cdlemk40f  31653  cdleml9  31718  dihmeetlem3N  32040  dochkrshp  32121  dihprrn  32161  dihjat1  32164  dvh3dim  32181  dochkrsm  32193  dochexmid  32203  lcfl7lem  32234  lcfl9a  32240  lclkrlem1  32241  mapdspex  32403  mapdindp2  32456  mapdh6dN  32474  hdmap1l6d  32549  hdmap11lem2  32580  hdmap14lem4a  32609  hdmapip0  32653  hlhilset  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator