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

Theorem sylan9eqr 2487
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 2485 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 450 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426
This theorem is referenced by:  sbcied2  3212  csbied2  3303  fun2ssres  5447  fcoi1  5573  fcoi2  5574  funssfv  5693  fvtp1  5912  nvof1o  5974  onuninsuci  6440  ot1stg  6580  ot2ndg  6581  mpt2mptsx  6626  dmmpt2ssx  6628  fmpt2x  6629  2ndconst  6651  mpt2xopoveq  6725  rdgeq12  6855  rdgsucmptnf  6871  frsucmptn  6880  abianfplem  6899  oev2  6951  oesuclem  6953  oawordeulem  6981  om00  7002  omass  7007  oeoa  7024  oeoe  7026  nnmass  7051  oaabs2  7072  omabs  7074  omxpenlem  7400  sbthlem4  7412  sbthlem6  7414  fodomr  7450  ssenen  7473  fi0  7658  cantnfp1  7877  cantnfp1OLD  7903  cnfcomlem  7920  cnfcomlemOLD  7928  cardaleph  8247  cflim2  8420  axdc4lem  8612  fpwwe2lem12  8795  fpwwe2lem13  8796  rankcf  8931  inatsk  8932  ltrnq  9135  addclprlem1  9172  mulclprlem  9175  1idpr  9185  prlem936  9203  reclem3pr  9205  mulcmpblnrlem  9227  recexsrlem  9257  map2psrpr  9264  nnnn0addcl  10597  zindd  10730  qaddcl  10956  qmulcl  10958  qreccl  10960  xaddnemnf  11191  xaddnepnf  11192  xaddcom  11195  xnegdi  11198  xaddass  11199  xpncan  11201  xleadd1a  11203  xlt2add  11210  rexmul  11221  xmulgt0  11233  xmulge0  11234  xmulasslem3  11236  xlemul1a  11238  xadddilem  11244  xadddi2  11247  modm1p1mod0  11733  seqf1olem2  11829  expp1  11855  expneg  11856  expcllem  11859  mulexp  11886  expmul  11892  bcpasc  12080  fseq1hash  12122  hashinfxadd  12131  hashge2el2dif  12167  hashfzo  12173  ffzohash  12175  fseq0hash  12177  fz0hash  12186  hashf1lem1  12191  brfi1indlem  12201  wrdf  12223  lsw0  12250  ccatval1  12259  ccatval2  12260  swrdval  12296  splval  12376  repswswrd  12405  s4dom  12512  wrdlen2i  12529  shftfn  12545  reim0b  12591  cjexp  12622  sqeqd  12638  fsumser  13190  sumsn  13200  binomlem  13274  expcnv  13308  ef0lem  13346  dvdsnegb  13532  sadadd2lem2  13628  gcdabs  13699  coprmdvds  13770  mulgcddvds  13772  pcge0  13910  pcadd  13933  pcmpt2  13937  prmreclem4  13962  ramval  14051  ramcl  14072  ressid2  14208  ressval2  14209  mrcmndind  15475  frmdval  15508  mulgfval  15607  mulgnn0subcl  15619  mulgnn0z  15626  isga  15788  symgval  15863  symgextfve  15903  symgfixf1  15922  f1omvdco2  15933  odid  16020  gexid  16059  frgpuptinv  16247  frgpup2  16252  dprdsn  16506  isabvd  16828  issrng  16858  lvecinv  17115  lspdisj2  17129  lspfixed  17130  lspexch  17131  sralem  17179  srasca  17183  sravsca  17184  sraip  17185  mplval  17434  opsrval  17487  znval  17807  psgndiflemB  17871  isphl  17898  mdetunilem7  18265  mdetuni0  18268  gsummatr01lem3  18304  gsummatr01lem4  18305  gsummatr01  18306  slesolinvbi  18328  indistopon  18446  0ntr  18516  pnrmopn  18788  kgenval  18949  pt1hmeo  19220  fmval  19357  fmf  19359  istmd  19486  istgp  19489  tsmsval2  19541  isxmet2d  19743  xpsxmetlem  19795  xpsmet  19798  blfvalps  19799  tmsval  19897  isnlm  20097  nmoleub  20151  idnghm  20163  blssioo  20213  blcvx  20216  icccvx  20363  pcorevlem  20439  isclm  20477  caufval  20627  iscms  20697  mbfsup  20983  i1f1  21009  dvexp3  21291  rolle  21303  dvivth  21323  evl1fval  21377  deg1add  21459  0dgr  21597  coefv0  21599  elqaalem2  21670  dvradcnv  21770  abelthlem8  21788  efper  21825  logtayl  21989  abscxpbnd  22075  dcubic2  22123  rlimcnp2  22244  cvxcl  22262  vmaval  22335  chtub  22435  logexprlim  22448  dchrsum2  22491  sumdchr2  22493  bposlem2  22508  lgsdir  22553  lgsne0  22556  lgsdirnn0  22562  lgsdinn0  22563  lgsquadlem2  22578  dchrvmasum2if  22630  dchrvmasumiflem1  22634  rpvmasum2  22645  pntpbnd1  22719  ostth2lem4  22769  ax5seglem1  22996  ax5seglem2  22997  ax5seglem5  23001  usgraedgprv  23117  vdgr1d  23395  vdgr1b  23396  vdgr1a  23398  eupatrl  23411  grpoidinvlem2  23514  grposn  23524  gxnn0neg  23572  gxid  23582  vcz  23770  nvz  23879  lnon0  24020  ipasslem2  24054  htthlem  24141  hvpncan  24263  hiidge0  24322  normgt0  24351  hsn0elch  24473  shsel3  24540  spansneleq  24795  normcan  24801  h1datomi  24806  fh1  24843  spansncvi  24877  5oalem1  24879  5oalem3  24881  5oalem5  24883  3oalem2  24888  pjdsi  24937  kbpj  25182  0hmop  25209  0lnfn  25211  adj0  25220  nlelshi  25286  branmfn  25331  opsqrlem1  25366  hst1h  25453  mdsl0  25536  superpos  25580  sumdmdlem  25644  cdj3lem1  25660  xrpxdivcld  25932  xrge0npcan  25980  resvid2  26149  resvval2  26150  esumsn  26368  esummulc1  26383  measxun2  26477  probun  26649  zetacvg  26848  lgamgulmlem2  26863  subdivcomb2  27231  prodsn  27319  dfrdg2  27455  wfrlem10  27579  bpolylem  28037  bpoly2  28046  bpoly3  28047  mblfinlem2  28270  mblfinlem3  28271  ismblfin  28273  mbfposadd  28280  itg2addnclem  28284  itg2addnclem3  28286  itg2addnc  28287  ftc1anclem8  28315  areacirc  28330  ismtyval  28540  ismrer1  28578  rabeq12f  28810  csbeq12  28811  bezoutr1  29171  jm2.26a  29191  sumsnd  29590  stoweidlem34  29672  el2xptp0  29970  hashrabsn01  30075  reuccats1  30104  ccatw2s1p1  30112  ccatw2s1p2  30113  wwlknimp  30164  wwlknextbi  30200  wwlkextwrd  30203  clwlkisclwwlklem2fv1  30287  clwlkisclwwlklem2a4  30289  clwlkisclwwlklem0  30293  clwwlkf  30299  clwwlkf1  30301  wwlkext2clwwlk  30308  clwwisshclww  30314  erclwwlkeqlen  30325  cshwlemma1  30332  eleclclwwlknlem2  30334  erclwwlkneqlen  30341  usghashecclwwlk  30352  vdcusgra  30374  cusgraisrusgra  30394  rusgra0edg  30416  usg2spot2nb  30501  dmmpt2ssx2  30568  zlmodzxzscm  30585  zlmodzxzadd  30586  psgnsn  30599  lmod0rng  30607  domnmsuppn0  30610  rmsuppss  30611  scmsuppss  30613  ldepsprlem  30712  lincresunit2  30718  bnj517  31577  bj-bary1lem1  32172  lsatcv1  32263  glbconN  32591  atltcvr  32649  3dim2  32682  islln2a  32731  2at0mat0  32739  islpln2a  32762  islvol2aN  32806  pmodlem2  33061  pmapjat1  33067  pcl0bN  33137  osumclN  33181  pexmidALTN  33192  lhp2at0nle  33249  4atexlemunv  33280  cdleme18b  33506  cdleme31sn1  33595  cdleme31sde  33599  cdleme31sn2  33603  ltrniotavalbN  33798  trljco  33954  cdlemh  34031  cdlemk40t  34132  cdlemk40f  34133  cdleml9  34198  dihmeetlem3N  34520  dochkrshp  34601  dihprrn  34641  dihjat1  34644  dvh3dim  34661  dochkrsm  34673  dochexmid  34683  lcfl7lem  34714  lcfl9a  34720  lclkrlem1  34721  mapdspex  34883  mapdindp2  34936  mapdh6dN  34954  hdmap1l6d  35029  hdmap11lem2  35060  hdmap14lem4a  35089  hdmapip0  35133  hlhilset  35152
  Copyright terms: Public domain W3C validator