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

Theorem sylan9eqr 2506
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 2504 . 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 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2435
This theorem is referenced by:  sbcied2  3351  csbied2  3448  fun2ssres  5619  fcoi1  5749  fcoi2  5750  funssfv  5871  fvtp1  6103  nvof1o  6171  onuninsuci  6660  ot1stg  6799  ot2ndg  6800  el2xptp0  6829  mpt2mptsx  6848  dmmpt2ssx  6850  fmpt2x  6851  2ndconst  6874  mpt2xopoveq  6949  rdgeq12  7081  rdgsucmptnf  7097  frsucmptn  7106  oev2  7175  oesuclem  7177  oawordeulem  7205  om00  7226  omass  7231  oeoa  7248  oeoe  7250  nnmass  7275  oaabs2  7296  omabs  7298  omxpenlem  7620  sbthlem4  7632  sbthlem6  7634  fodomr  7670  ssenen  7693  fi0  7882  cantnfp1  8103  cantnfp1OLD  8129  cnfcomlem  8146  cnfcomlemOLD  8154  cardaleph  8473  cflim2  8646  axdc4lem  8838  fpwwe2lem12  9022  fpwwe2lem13  9023  rankcf  9158  inatsk  9159  ltrnq  9360  addclprlem1  9397  mulclprlem  9400  1idpr  9410  prlem936  9428  reclem3pr  9430  mulcmpblnrlem  9450  recexsrlem  9483  map2psrpr  9490  nnnn0addcl  10833  zindd  10971  qaddcl  11208  qmulcl  11210  qreccl  11212  xaddnemnf  11443  xaddnepnf  11444  xaddcom  11447  xnegdi  11450  xaddass  11451  xpncan  11453  xleadd1a  11455  xlt2add  11462  rexmul  11473  xmulgt0  11485  xmulge0  11486  xmulasslem3  11488  xlemul1a  11490  xadddilem  11496  xadddi2  11499  modm1p1mod0  12019  seqf1olem2  12128  expp1  12154  expneg  12155  expcllem  12158  mulexp  12186  expmul  12192  bcpasc  12380  hashrabsn01  12422  fseq1hash  12425  hashinfxadd  12434  hashfzo  12468  ffzo0hash  12470  fz0hash  12480  hashf1lem1  12485  hashge2el2dif  12502  brfi1indlem  12512  lsw0  12567  ccatval1  12576  ccatval2  12577  ccatw2s1p1  12621  ccatw2s1p2  12622  swrdval  12625  reuccats1  12687  splval  12708  repswswrd  12737  2cshwcshw  12774  s4dom  12848  wrdlen2i  12865  shftfn  12887  reim0b  12933  cjexp  12964  sqeqd  12980  fsumser  13533  sumsn  13544  binomlem  13622  expcnv  13656  prodsn  13748  ef0lem  13795  dvdsnegb  13982  sadadd2lem2  14081  gcdabs  14152  coprmdvds  14224  mulgcddvds  14226  pcge0  14366  pcadd  14389  pcmpt2  14393  prmreclem4  14418  ramval  14507  ramcl  14528  ressid2  14666  ressval2  14667  mrcmndind  15975  frmdval  15997  mgm2nsgrplem3  16016  mulgfval  16121  mulgnn0subcl  16133  mulgnn0z  16140  isga  16307  symgval  16382  symgextfve  16422  symgfixf1  16440  f1omvdco2  16451  psgnsn  16523  odid  16540  gexid  16579  frgpuptinv  16767  frgpup2  16772  dprdsn  17061  srgmulgass  17160  srgpcomp  17161  srgbinomlem4  17172  f1rhm0to0  17367  f1rhm0to0ALT  17368  isabvd  17447  issrng  17477  lmodvsmmulgdi  17525  mptscmfsupp0  17554  lvecinv  17737  lspdisj2  17751  lspfixed  17752  lspexch  17753  sralem  17801  srasca  17805  sravsca  17806  sraip  17807  assamulgscmlem2  17976  mplval  18062  opsrval  18117  cply1mul  18313  gsummoncoe1  18324  evl1fval  18342  znval  18549  psgndiflemB  18613  isphl  18640  scmate  18989  scmatscm  18992  mdetdiagid  19079  mdetunilem7  19097  mdetuni0  19100  gsummatr01lem3  19136  gsummatr01lem4  19137  gsummatr01  19138  slesolinvbi  19160  cpmatacl  19194  cpmatinvcl  19195  pmatcollpw2lem  19255  monmatcollpw  19257  pmatcollpwfi  19260  mp2pm2mplem4  19287  pm2mp  19303  cpmadugsumlemF  19354  cpmadugsumfi  19355  cpmadumatpoly  19361  cayhamlem4  19366  cayleyhamilton0  19367  cayleyhamiltonALT  19369  indistopon  19479  0ntr  19549  pnrmopn  19821  reftr  19992  kgenval  20013  pt1hmeo  20284  fmval  20421  fmf  20423  istmd  20550  istgp  20553  tsmsval2  20605  isxmet2d  20807  xpsxmetlem  20859  xpsmet  20862  blfvalps  20863  tmsval  20961  isnlm  21161  nmoleub  21215  idnghm  21227  blssioo  21277  blcvx  21280  icccvx  21427  pcorevlem  21503  isclm  21541  caufval  21691  iscms  21761  mbfsup  22048  i1f1  22074  dvexp3  22356  rolle  22368  dvivth  22388  deg1add  22481  0dgr  22619  coefv0  22621  elqaalem2  22692  dvradcnv  22792  abelthlem8  22810  efper  22848  logtayl  23017  abscxpbnd  23103  dcubic2  23151  rlimcnp2  23272  cvxcl  23290  vmaval  23363  chtub  23463  logexprlim  23476  dchrsum2  23519  sumdchr2  23521  bposlem2  23536  lgsdir  23581  lgsne0  23584  lgsdirnn0  23590  lgsdinn0  23591  lgsquadlem2  23606  dchrvmasum2if  23658  dchrvmasumiflem1  23662  rpvmasum2  23673  pntpbnd1  23747  ostth2lem4  23797  trgcgrg  23882  ax5seglem1  24207  ax5seglem2  24208  ax5seglem5  24212  usgraedgprv  24352  wwlknimp  24663  wwlknextbi  24701  wwlkextwrd  24704  clwlkisclwwlklem2fv1  24758  clwlkisclwwlklem2a4  24760  clwlkisclwwlklem0  24764  clwwlkf  24770  clwwlkf1  24772  wwlkext2clwwlk  24779  clwwisshclww  24783  erclwwlkeqlen  24788  eleclclwwlknlem2  24794  erclwwlkneqlen  24800  usghashecclwwlk  24811  vdgr1d  24879  vdgr1b  24880  vdgr1a  24882  cusgraisrusgra  24914  rusgra0edg  24931  eupatrl  24944  usg2spot2nb  25041  grpoidinvlem2  25183  grposn  25193  gxnn0neg  25241  gxid  25251  vcz  25439  nvz  25548  lnon0  25689  ipasslem2  25723  htthlem  25810  hvpncan  25932  hiidge0  25991  normgt0  26020  hsn0elch  26142  shsel3  26209  spansneleq  26464  normcan  26470  h1datomi  26475  fh1  26512  spansncvi  26546  5oalem1  26548  5oalem3  26550  5oalem5  26552  3oalem2  26557  pjdsi  26606  kbpj  26851  0hmop  26878  0lnfn  26880  adj0  26889  nlelshi  26955  branmfn  27000  opsqrlem1  27035  hst1h  27122  mdsl0  27205  superpos  27249  sumdmdlem  27313  cdj3lem1  27329  xrpxdivcld  27608  2sqn0  27611  xrge0npcan  27661  resvid2  27795  resvval2  27796  esumsn  28049  esummulc1  28064  measxun2  28158  sibfof  28259  probun  28335  zetacvg  28534  lgamgulmlem2  28549  mrsubfval  28845  msrval  28875  subdivcomb2  29083  dfrdg2  29203  wfrlem10  29327  bpolylem  29785  bpoly2  29794  bpoly3  29795  mblfinlem2  30027  mblfinlem3  30028  ismblfin  30030  mbfposadd  30037  itg2addnclem  30041  itg2addnclem3  30043  itg2addnc  30044  ftc1anclem8  30072  areacirc  30087  ismtyval  30271  ismrer1  30309  rabeq12f  30540  csbeq12  30541  iuneq12f  30547  bezoutr1  30899  jm2.26a  30917  radcnvrat  31171  dvdslcm  31180  lcmeq0  31182  lcmcl  31183  lcmabs  31187  lcmgcdlem  31188  lcmdvds  31190  sumsnd  31355  icccncfext  31597  fperdvper  31619  dvcosax  31627  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  volioc  31661  itgiccshift  31669  stoweidlem34  31705  dirkercncflem2  31775  fourierdlem32  31810  fourierdlem41  31819  fourierdlem48  31826  fourierdlem64  31842  fourierdlem73  31851  fourierdlem79  31857  fourierdlem82  31860  fourierdlem97  31875  fourierdlem101  31879  fourierdlem109  31887  fourierdlem111  31889  fouriersw  31903  vdcusgra  32197  clintopval  32365  2zrngagrp  32459  rngcval  32510  ringcval  32553  dmmpt2ssx2  32659  zlmodzxzscm  32679  zlmodzxzadd  32680  lmod0rng  32694  domnmsuppn0  32697  rmsuppss  32698  scmsuppss  32700  ply1mulgsumlem4  32724  ldepsprlem  32808  lincresunit2  32814  bnj517  33676  bj-bary1lem1  34420  lsatcv1  34513  glbconN  34841  atltcvr  34899  3dim2  34932  islln2a  34981  2at0mat0  34989  islpln2a  35012  islvol2aN  35056  pmodlem2  35311  pmapjat1  35317  pcl0bN  35387  osumclN  35431  pexmidALTN  35442  lhp2at0nle  35499  4atexlemunv  35530  cdleme18b  35757  cdleme31sn1  35847  cdleme31sde  35851  cdleme31sn2  35855  ltrniotavalbN  36050  trljco  36206  cdlemh  36283  cdlemk40t  36384  cdlemk40f  36385  cdleml9  36450  dihmeetlem3N  36772  dochkrshp  36853  dihprrn  36893  dihjat1  36896  dvh3dim  36913  dochkrsm  36925  dochexmid  36935  lcfl7lem  36966  lcfl9a  36972  lclkrlem1  36973  mapdspex  37135  mapdindp2  37188  mapdh6dN  37206  hdmap1l6d  37281  hdmap11lem2  37312  hdmap14lem4a  37341  hdmapip0  37385  hlhilset  37404
  Copyright terms: Public domain W3C validator