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

Theorem sylan9eqr 2337
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 2335 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 439 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623
This theorem is referenced by:  sbcied2  3028  csbied2  3124  onuninsuci  4631  fun2ssres  5295  fcoi1  5415  fcoi2  5416  funssfv  5543  fvtp1  5724  ot1stg  6134  ot2ndg  6135  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  2ndconst  6208  rdgeq12  6426  rdgsucmptnf  6442  frsucmptn  6451  abianfplem  6470  oev2  6522  oesuclem  6524  oawordeulem  6552  om00  6573  omass  6578  oeoa  6595  oeoe  6597  nnmass  6622  oaabs2  6643  omabs  6645  omxpenlem  6963  sbthlem4  6974  sbthlem6  6976  fodomr  7012  ssenen  7035  fi0  7173  cantnfp1  7383  cnfcomlem  7402  cardaleph  7716  cflim2  7889  axdc4lem  8081  fpwwe2lem12  8263  fpwwe2lem13  8264  rankcf  8399  inatsk  8400  ltrnq  8603  addclprlem1  8640  mulclprlem  8643  1idpr  8653  prlem936  8671  reclem3pr  8673  mulcmpblnrlem  8695  recexsrlem  8725  map2psrpr  8732  nnnn0addcl  9995  zindd  10113  qaddcl  10332  qmulcl  10334  qreccl  10336  xaddnemnf  10561  xaddnepnf  10562  xaddcom  10565  xnegdi  10568  xaddass  10569  xpncan  10571  xleadd1a  10573  xlt2add  10580  rexmul  10591  xmulgt0  10603  xmulge0  10604  xmulasslem3  10606  xlemul1a  10608  xadddilem  10614  xadddi2  10617  seqf1olem2  11086  expp1  11110  expneg  11111  expcllem  11114  mulexp  11141  expmul  11147  bcpasc  11333  fseq1hash  11358  hashfzo  11383  hashf1lem1  11393  wrdf  11419  ccatval1  11431  ccatval2  11432  swrdval  11450  splval  11466  shftfn  11568  reim0b  11604  cjexp  11635  sqeqd  11651  fsumser  12203  sumsn  12213  binomlem  12287  expcnv  12322  ef0lem  12360  dvdsnegb  12546  sadadd2lem2  12641  gcdabs  12712  coprmdvds  12781  mulgcddvds  12783  pcge0  12914  pcadd  12937  pcmpt2  12941  prmreclem4  12966  ramval  13055  ramcl  13076  ressid2  13196  ressval2  13197  frmdval  14473  mulgfval  14568  mulgnn0subcl  14580  mulgnn0z  14587  isga  14745  symgval  14771  odid  14853  gexid  14892  frgpuptinv  15080  frgpup2  15085  dprdsn  15271  isabvd  15585  issrng  15615  lvecinv  15866  lspdisj2  15880  lspfixed  15881  lspexch  15882  sralem  15930  srasca  15934  sravsca  15935  mplval  16173  opsrval  16216  znval  16489  isphl  16532  indistopon  16738  0ntr  16808  pnrmopn  17071  kgenval  17230  pt1hmeo  17497  fmval  17638  fmf  17640  istmd  17757  istgp  17760  tsmsval2  17812  isxmet2d  17892  xpsxmetlem  17943  xpsmet  17946  blfval  17947  tmsval  18027  isnlm  18186  nmoleub  18240  idnghm  18252  blssioo  18301  blcvx  18304  icccvx  18448  pcorevlem  18524  isclm  18562  caufval  18701  iscms  18767  mbfsup  19019  i1f1  19045  dvexp3  19325  rolle  19337  dvivth  19357  evl1fval  19410  deg1add  19489  0dgr  19627  coefv0  19629  elqaalem2  19700  dvradcnv  19797  abelthlem8  19815  efper  19847  logtayl  20007  abscxpbnd  20093  dcubic2  20140  rlimcnp2  20261  cvxcl  20279  vmaval  20351  chtub  20451  logexprlim  20464  dchrsum2  20507  sumdchr2  20509  bposlem2  20524  lgsdir  20569  lgsne0  20572  lgsdirnn0  20578  lgsdinn0  20579  lgsquadlem2  20594  dchrvmasum2if  20646  dchrvmasumiflem1  20650  rpvmasum2  20661  pntpbnd1  20735  ostth2lem4  20785  grpoidinvlem2  20872  grposn  20882  gxnn0neg  20930  gxid  20940  vcz  21126  nvz  21235  lnon0  21376  ipasslem2  21410  htthlem  21497  hvpncan  21618  hiidge0  21677  normgt0  21706  hsn0elch  21827  shsel3  21894  spansneleq  22149  normcan  22155  h1datomi  22160  fh1  22197  spansncvi  22231  5oalem1  22233  5oalem3  22235  5oalem5  22237  3oalem2  22242  pjdsi  22291  kbpj  22536  0hmop  22563  0lnfn  22565  adj0  22574  nlelshi  22640  branmfn  22685  opsqrlem1  22720  hst1h  22807  mdsl0  22890  superpos  22934  sumdmdlem  22998  cdj3lem1  23014  nvof1o  23036  xrpxdivcld  23119  esumsn  23437  measxun2  23538  probun  23622  zetacvg  23689  vdgr1d  23894  vdgr1b  23895  vdgr1a  23897  subdivcomb2  24091  dfrdg2  24152  ax5seglem1  24556  ax5seglem2  24557  ax5seglem5  24561  bpolylem  24783  bpoly2  24792  bpoly3  24793  areacirc  24931  sssu  25141  1ded  25738  idfisf  25841  ismtyval  26524  ismrer1  26562  bezoutr1  27073  jm2.26a  27093  f1omvdco2  27391  sumsnd  27697  mpt2xopoveq  28085  s4dom  28092  usgraedgprv  28122  bnj517  28917  lsatcv1  29238  glbconN  29566  atltcvr  29624  3dim2  29657  islln2a  29706  2at0mat0  29714  islpln2a  29737  islvol2aN  29781  pmodlem2  30036  pmapjat1  30042  pcl0bN  30112  osumclN  30156  pexmidALTN  30167  lhp2at0nle  30224  4atexlemunv  30255  cdleme18b  30481  cdleme31sn1  30570  cdleme31sde  30574  cdleme31sn2  30578  ltrniotavalbN  30773  trljco  30929  cdlemh  31006  cdlemk40t  31107  cdlemk40f  31108  cdleml9  31173  dihmeetlem3N  31495  dochkrshp  31576  dihprrn  31616  dihjat1  31619  dvh3dim  31636  dochkrsm  31648  dochexmid  31658  lcfl7lem  31689  lcfl9a  31695  lclkrlem1  31696  mapdspex  31858  mapdindp2  31911  mapdh6dN  31929  hdmap1l6d  32004  hdmap11lem2  32035  hdmap14lem4a  32064  hdmapip0  32108  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator