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

Theorem sylan9eqr 2497
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 2495 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 453 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436
This theorem is referenced by:  sbcied2  3245  csbied2  3336  fun2ssres  5480  fcoi1  5606  fcoi2  5607  funssfv  5726  fvtp1  5946  nvof1o  6008  onuninsuci  6472  ot1stg  6612  ot2ndg  6613  mpt2mptsx  6658  dmmpt2ssx  6660  fmpt2x  6661  2ndconst  6683  mpt2xopoveq  6757  rdgeq12  6890  rdgsucmptnf  6906  frsucmptn  6915  oev2  6984  oesuclem  6986  oawordeulem  7014  om00  7035  omass  7040  oeoa  7057  oeoe  7059  nnmass  7084  oaabs2  7105  omabs  7107  omxpenlem  7433  sbthlem4  7445  sbthlem6  7447  fodomr  7483  ssenen  7506  fi0  7691  cantnfp1  7910  cantnfp1OLD  7936  cnfcomlem  7953  cnfcomlemOLD  7961  cardaleph  8280  cflim2  8453  axdc4lem  8645  fpwwe2lem12  8829  fpwwe2lem13  8830  rankcf  8965  inatsk  8966  ltrnq  9169  addclprlem1  9206  mulclprlem  9209  1idpr  9219  prlem936  9237  reclem3pr  9239  mulcmpblnrlem  9261  recexsrlem  9291  map2psrpr  9298  nnnn0addcl  10631  zindd  10764  qaddcl  10990  qmulcl  10992  qreccl  10994  xaddnemnf  11225  xaddnepnf  11226  xaddcom  11229  xnegdi  11232  xaddass  11233  xpncan  11235  xleadd1a  11237  xlt2add  11244  rexmul  11255  xmulgt0  11267  xmulge0  11268  xmulasslem3  11270  xlemul1a  11272  xadddilem  11278  xadddi2  11281  modm1p1mod0  11771  seqf1olem2  11867  expp1  11893  expneg  11894  expcllem  11897  mulexp  11924  expmul  11930  bcpasc  12118  fseq1hash  12160  hashinfxadd  12169  hashge2el2dif  12205  hashfzo  12211  ffzohash  12213  fseq0hash  12215  fz0hash  12224  hashf1lem1  12229  brfi1indlem  12239  wrdf  12261  lsw0  12288  ccatval1  12297  ccatval2  12298  swrdval  12334  splval  12414  repswswrd  12443  s4dom  12550  wrdlen2i  12567  shftfn  12583  reim0b  12629  cjexp  12660  sqeqd  12676  fsumser  13228  sumsn  13238  binomlem  13313  expcnv  13347  ef0lem  13385  dvdsnegb  13571  sadadd2lem2  13667  gcdabs  13738  coprmdvds  13809  mulgcddvds  13811  pcge0  13949  pcadd  13972  pcmpt2  13976  prmreclem4  14001  ramval  14090  ramcl  14111  ressid2  14247  ressval2  14248  mrcmndind  15515  frmdval  15550  mulgfval  15649  mulgnn0subcl  15661  mulgnn0z  15668  isga  15830  symgval  15905  symgextfve  15945  symgfixf1  15964  f1omvdco2  15975  odid  16062  gexid  16101  frgpuptinv  16289  frgpup2  16294  dprdsn  16555  srgmulgass  16652  srgpcomp  16653  srgbinomlem4  16663  f1rhm0to0  16850  f1rhm0to0ALT  16851  isabvd  16927  issrng  16957  mptscmfsupp0  17033  lvecinv  17216  lspdisj2  17230  lspfixed  17231  lspexch  17232  sralem  17280  srasca  17284  sravsca  17285  sraip  17286  mplval  17523  opsrval  17578  evl1fval  17784  znval  17988  psgndiflemB  18052  isphl  18079  mdetunilem7  18446  mdetuni0  18449  gsummatr01lem3  18485  gsummatr01lem4  18486  gsummatr01  18487  slesolinvbi  18509  indistopon  18627  0ntr  18697  pnrmopn  18969  kgenval  19130  pt1hmeo  19401  fmval  19538  fmf  19540  istmd  19667  istgp  19670  tsmsval2  19722  isxmet2d  19924  xpsxmetlem  19976  xpsmet  19979  blfvalps  19980  tmsval  20078  isnlm  20278  nmoleub  20332  idnghm  20344  blssioo  20394  blcvx  20397  icccvx  20544  pcorevlem  20620  isclm  20658  caufval  20808  iscms  20878  mbfsup  21164  i1f1  21190  dvexp3  21472  rolle  21484  dvivth  21504  deg1add  21597  0dgr  21735  coefv0  21737  elqaalem2  21808  dvradcnv  21908  abelthlem8  21926  efper  21963  logtayl  22127  abscxpbnd  22213  dcubic2  22261  rlimcnp2  22382  cvxcl  22400  vmaval  22473  chtub  22573  logexprlim  22586  dchrsum2  22629  sumdchr2  22631  bposlem2  22646  lgsdir  22691  lgsne0  22694  lgsdirnn0  22700  lgsdinn0  22701  lgsquadlem2  22716  dchrvmasum2if  22768  dchrvmasumiflem1  22772  rpvmasum2  22783  pntpbnd1  22857  ostth2lem4  22907  ax5seglem1  23196  ax5seglem2  23197  ax5seglem5  23201  usgraedgprv  23317  vdgr1d  23595  vdgr1b  23596  vdgr1a  23598  eupatrl  23611  grpoidinvlem2  23714  grposn  23724  gxnn0neg  23772  gxid  23782  vcz  23970  nvz  24079  lnon0  24220  ipasslem2  24254  htthlem  24341  hvpncan  24463  hiidge0  24522  normgt0  24551  hsn0elch  24673  shsel3  24740  spansneleq  24995  normcan  25001  h1datomi  25006  fh1  25043  spansncvi  25077  5oalem1  25079  5oalem3  25081  5oalem5  25083  3oalem2  25088  pjdsi  25137  kbpj  25382  0hmop  25409  0lnfn  25411  adj0  25420  nlelshi  25486  branmfn  25531  opsqrlem1  25566  hst1h  25653  mdsl0  25736  superpos  25780  sumdmdlem  25844  cdj3lem1  25860  xrpxdivcld  26132  xrge0npcan  26179  resvid2  26318  resvval2  26319  esumsn  26537  esummulc1  26552  measxun2  26646  probun  26824  zetacvg  27023  lgamgulmlem2  27038  subdivcomb2  27407  prodsn  27495  dfrdg2  27631  wfrlem10  27755  bpolylem  28213  bpoly2  28222  bpoly3  28223  mblfinlem2  28455  mblfinlem3  28456  ismblfin  28458  mbfposadd  28465  itg2addnclem  28469  itg2addnclem3  28471  itg2addnc  28472  ftc1anclem8  28500  areacirc  28515  ismtyval  28725  ismrer1  28763  rabeq12f  28995  csbeq12  28996  iuneq12f  29002  bezoutr1  29355  jm2.26a  29375  sumsnd  29774  stoweidlem34  29855  el2xptp0  30153  hashrabsn01  30258  reuccats1  30287  ccatw2s1p1  30295  ccatw2s1p2  30296  wwlknimp  30347  wwlknextbi  30383  wwlkextwrd  30386  clwlkisclwwlklem2fv1  30470  clwlkisclwwlklem2a4  30472  clwlkisclwwlklem0  30476  clwwlkf  30482  clwwlkf1  30484  wwlkext2clwwlk  30491  clwwisshclww  30497  erclwwlkeqlen  30508  cshwlemma1  30515  eleclclwwlknlem2  30517  erclwwlkneqlen  30524  usghashecclwwlk  30535  vdcusgra  30557  cusgraisrusgra  30577  rusgra0edg  30599  usg2spot2nb  30684  dmmpt2ssx2  30754  zlmodzxzscm  30783  zlmodzxzadd  30784  psgnsn  30801  lmod0rng  30809  domnmsuppn0  30812  rmsuppss  30813  scmsuppss  30815  lmodvsmmulgdi  30846  assamulgscmlem2  30854  gsummoncoe1  30876  ply1mulgsumlem4  30880  cply1mul  30884  scmatsubcl  30923  mdetdiagid  30934  ldepsprlem  31003  lincresunit2  31009  cnstpmatacl  31068  cnstpmatinvcl  31069  pmatcollpw2lem  31120  mp2pm2mplem4  31134  bnj517  31974  bj-bary1lem1  32696  lsatcv1  32789  glbconN  33117  atltcvr  33175  3dim2  33208  islln2a  33257  2at0mat0  33265  islpln2a  33288  islvol2aN  33332  pmodlem2  33587  pmapjat1  33593  pcl0bN  33663  osumclN  33707  pexmidALTN  33718  lhp2at0nle  33775  4atexlemunv  33806  cdleme18b  34032  cdleme31sn1  34121  cdleme31sde  34125  cdleme31sn2  34129  ltrniotavalbN  34324  trljco  34480  cdlemh  34557  cdlemk40t  34658  cdlemk40f  34659  cdleml9  34724  dihmeetlem3N  35046  dochkrshp  35127  dihprrn  35167  dihjat1  35170  dvh3dim  35187  dochkrsm  35199  dochexmid  35209  lcfl7lem  35240  lcfl9a  35246  lclkrlem1  35247  mapdspex  35409  mapdindp2  35462  mapdh6dN  35480  hdmap1l6d  35555  hdmap11lem2  35586  hdmap14lem4a  35615  hdmapip0  35659  hlhilset  35678
  Copyright terms: Public domain W3C validator