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

Theorem sylan9eqr 2350
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 2348 . 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 1632
This theorem is referenced by:  sbcied2  3041  csbied2  3137  onuninsuci  4647  fun2ssres  5311  fcoi1  5431  fcoi2  5432  funssfv  5559  fvtp1  5740  ot1stg  6150  ot2ndg  6151  mpt2mptsx  6203  dmmpt2ssx  6205  fmpt2x  6206  2ndconst  6224  rdgeq12  6442  rdgsucmptnf  6458  frsucmptn  6467  abianfplem  6486  oev2  6538  oesuclem  6540  oawordeulem  6568  om00  6589  omass  6594  oeoa  6611  oeoe  6613  nnmass  6638  oaabs2  6659  omabs  6661  omxpenlem  6979  sbthlem4  6990  sbthlem6  6992  fodomr  7028  ssenen  7051  fi0  7189  cantnfp1  7399  cnfcomlem  7418  cardaleph  7732  cflim2  7905  axdc4lem  8097  fpwwe2lem12  8279  fpwwe2lem13  8280  rankcf  8415  inatsk  8416  ltrnq  8619  addclprlem1  8656  mulclprlem  8659  1idpr  8669  prlem936  8687  reclem3pr  8689  mulcmpblnrlem  8711  recexsrlem  8741  map2psrpr  8748  nnnn0addcl  10011  zindd  10129  qaddcl  10348  qmulcl  10350  qreccl  10352  xaddnemnf  10577  xaddnepnf  10578  xaddcom  10581  xnegdi  10584  xaddass  10585  xpncan  10587  xleadd1a  10589  xlt2add  10596  rexmul  10607  xmulgt0  10619  xmulge0  10620  xmulasslem3  10622  xlemul1a  10624  xadddilem  10630  xadddi2  10633  seqf1olem2  11102  expp1  11126  expneg  11127  expcllem  11130  mulexp  11157  expmul  11163  bcpasc  11349  fseq1hash  11374  hashfzo  11399  hashf1lem1  11409  wrdf  11435  ccatval1  11447  ccatval2  11448  swrdval  11466  splval  11482  shftfn  11584  reim0b  11620  cjexp  11651  sqeqd  11667  fsumser  12219  sumsn  12229  binomlem  12303  expcnv  12338  ef0lem  12376  dvdsnegb  12562  sadadd2lem2  12657  gcdabs  12728  coprmdvds  12797  mulgcddvds  12799  pcge0  12930  pcadd  12953  pcmpt2  12957  prmreclem4  12982  ramval  13071  ramcl  13092  ressid2  13212  ressval2  13213  frmdval  14489  mulgfval  14584  mulgnn0subcl  14596  mulgnn0z  14603  isga  14761  symgval  14787  odid  14869  gexid  14908  frgpuptinv  15096  frgpup2  15101  dprdsn  15287  isabvd  15601  issrng  15631  lvecinv  15882  lspdisj2  15896  lspfixed  15897  lspexch  15898  sralem  15946  srasca  15950  sravsca  15951  mplval  16189  opsrval  16232  znval  16505  isphl  16548  indistopon  16754  0ntr  16824  pnrmopn  17087  kgenval  17246  pt1hmeo  17513  fmval  17654  fmf  17656  istmd  17773  istgp  17776  tsmsval2  17828  isxmet2d  17908  xpsxmetlem  17959  xpsmet  17962  blfval  17963  tmsval  18043  isnlm  18202  nmoleub  18256  idnghm  18268  blssioo  18317  blcvx  18320  icccvx  18464  pcorevlem  18540  isclm  18578  caufval  18717  iscms  18783  mbfsup  19035  i1f1  19061  dvexp3  19341  rolle  19353  dvivth  19373  evl1fval  19426  deg1add  19505  0dgr  19643  coefv0  19645  elqaalem2  19716  dvradcnv  19813  abelthlem8  19831  efper  19863  logtayl  20023  abscxpbnd  20109  dcubic2  20156  rlimcnp2  20277  cvxcl  20295  vmaval  20367  chtub  20467  logexprlim  20480  dchrsum2  20523  sumdchr2  20525  bposlem2  20540  lgsdir  20585  lgsne0  20588  lgsdirnn0  20594  lgsdinn0  20595  lgsquadlem2  20610  dchrvmasum2if  20662  dchrvmasumiflem1  20666  rpvmasum2  20677  pntpbnd1  20751  ostth2lem4  20801  grpoidinvlem2  20888  grposn  20898  gxnn0neg  20946  gxid  20956  vcz  21142  nvz  21251  lnon0  21392  ipasslem2  21426  htthlem  21513  hvpncan  21634  hiidge0  21693  normgt0  21722  hsn0elch  21843  shsel3  21910  spansneleq  22165  normcan  22171  h1datomi  22176  fh1  22213  spansncvi  22247  5oalem1  22249  5oalem3  22251  5oalem5  22253  3oalem2  22258  pjdsi  22307  kbpj  22552  0hmop  22579  0lnfn  22581  adj0  22590  nlelshi  22656  branmfn  22701  opsqrlem1  22736  hst1h  22823  mdsl0  22906  superpos  22950  sumdmdlem  23014  cdj3lem1  23030  nvof1o  23052  xrpxdivcld  23135  esumsn  23452  measxun2  23553  probun  23637  zetacvg  23704  vdgr1d  23909  vdgr1b  23910  vdgr1a  23912  subdivcomb2  24106  faclimlem3  24119  dfrdg2  24223  ax5seglem1  24628  ax5seglem2  24629  ax5seglem5  24633  bpolylem  24855  bpoly2  24864  bpoly3  24865  itg2addnclem  25003  areacirc  25034  sssu  25244  1ded  25841  idfisf  25944  ismtyval  26627  ismrer1  26665  bezoutr1  27176  jm2.26a  27196  f1omvdco2  27494  sumsnd  27800  mpt2xopoveq  28201  s4dom  28224  usgraedgprv  28256  eupatrl  28385  bnj517  29233  lsatcv1  29860  glbconN  30188  atltcvr  30246  3dim2  30279  islln2a  30328  2at0mat0  30336  islpln2a  30359  islvol2aN  30403  pmodlem2  30658  pmapjat1  30664  pcl0bN  30734  osumclN  30778  pexmidALTN  30789  lhp2at0nle  30846  4atexlemunv  30877  cdleme18b  31103  cdleme31sn1  31192  cdleme31sde  31196  cdleme31sn2  31200  ltrniotavalbN  31395  trljco  31551  cdlemh  31628  cdlemk40t  31729  cdlemk40f  31730  cdleml9  31795  dihmeetlem3N  32117  dochkrshp  32198  dihprrn  32238  dihjat1  32241  dvh3dim  32258  dochkrsm  32270  dochexmid  32280  lcfl7lem  32311  lcfl9a  32317  lclkrlem1  32318  mapdspex  32480  mapdindp2  32533  mapdh6dN  32551  hdmap1l6d  32626  hdmap11lem2  32657  hdmap14lem4a  32686  hdmapip0  32730  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator