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

Theorem sylan9eq 2335
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1  |-  ( ph  ->  A  =  B )
sylan9eq.2  |-  ( ps 
->  B  =  C
)
Assertion
Ref Expression
sylan9eq  |-  ( (
ph  /\  ps )  ->  A  =  C )

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2  |-  ( ph  ->  A  =  B )
2 sylan9eq.2 . 2  |-  ( ps 
->  B  =  C
)
3 eqtr 2300 . 2  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
41, 2, 3syl2an 463 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623
This theorem is referenced by:  sylan9req  2336  sylan9eqr  2337  difeq12  3289  uneq12  3324  ineq12  3365  ifeq12  3578  ifbi  3582  preq12  3708  prprc  3738  preq12b  3788  opeq12  3798  opthwiener  4268  ordintdif  4441  xpeq12  4708  sosn  4759  nfimad  5021  coi2  5189  funimass1  5325  f1orescnv  5488  resdif  5494  fvmpt2  5608  fvmptnf  5617  oveq12  5867  cbvmpt2v  5926  ovmpt2g  5982  caofinvl  6104  eqopi  6156  fmpt2co  6202  rdgsucmptf  6441  frsucmpt  6450  abianfplem  6470  oevn0  6514  oa0r  6537  om1r  6541  oe1m  6543  omass  6578  oeoalem  6594  oeoa  6595  oeoe  6597  map0g  6807  xpcomco  6952  sbthlem4  6974  sbthlem5  6975  xpmapenlem  7028  phplem3  7042  phplem4  7043  unxpdomlem3  7069  ordtypelem7  7239  cardennn  7616  dfac9  7762  cdaassen  7808  alephsing  7902  axcc3  8064  ac6num  8106  konigthlem  8190  canthp1lem2  8275  ordpipq  8566  ltrnq  8603  addclprlem2  8641  mulclprlem  8643  prlem934  8657  prlem936  8671  mulcmpblnrlem  8695  addcnsr  8757  mulcnsr  8758  axcnre  8786  recex  9400  uzindOLD  10106  rpnnen1lem3  10344  rpnnen1lem5  10346  xaddpnf1  10553  xaddpnf2  10554  xaddmnf1  10555  xaddmnf2  10556  rexadd  10559  xaddnemnf  10561  xaddnepnf  10562  xadddilem  10614  om2uzrani  11015  om2uzrdg  11019  seqf1olem2  11086  seqf1o  11087  modexp  11236  faclbnd4lem3  11308  hashunsng  11367  swrdfv  11457  revfv  11481  shftcan1  11578  remul2  11615  immul2  11622  sumss  12197  geomulcvg  12332  ef0lem  12360  efieq1re  12479  rpnnen2lem1  12493  ruclem3  12511  dvdsnegb  12546  dvdscmul  12555  dvds2ln  12559  dvds2add  12560  dvds2sub  12561  gcdn0val  12689  rpmulgcd  12734  odzval  12856  pcval  12897  pcmpt  12940  prmreclem4  12966  1arithlem2  12971  vdwlem8  13035  ramcl2lem  13056  ramtcl  13057  ramtub  13059  ramcl2  13063  ramcl  13076  setsval  13172  prfcl  13977  curf1cl  14002  curfcl  14006  hofcl  14033  yonedalem4c  14051  lubval  14113  glbval  14118  joinval  14122  meetval  14129  psssdm  14325  grplactval  14563  cntzval  14797  odlem2  14854  gexlem2  14893  lsmvalx  14950  efgtval  15032  efgredlema  15049  vrgpval  15076  cyggex  15184  gsumcom2  15226  dvdsrtr  15434  abvtrivd  15605  lmhmco  15800  reslmhm  15809  lvecinv  15866  mplmon2  16234  subrgasclcl  16240  coe1fv  16287  zrhmulg  16464  znzrhval  16500  ocvval  16567  isopn3  16803  cnpval  16966  ptbasfi  17276  dfac14  17312  cnmptkk  17377  xkofvcn  17378  cnmptk1p  17379  cnmptk2  17380  xkocnv  17505  flfval  17685  ptcmplem3  17748  ptcmpg  17751  tmdmulg  17775  prdsxmslem2  18075  subgnm2  18150  nmoval  18224  fsum2cn  18375  pcovalg  18510  cphnm  18629  tchnmval  18660  ovolctb  18849  ioorcl  18932  uniioombllem2  18938  itg1addlem3  19053  itg1climres  19069  itg2uba  19098  itg2splitlem  19103  elcpn  19283  dvexp  19302  dvexp2  19303  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  dvlip2  19342  dveq0  19347  dv11cn  19348  lhop1lem  19360  lhop2  19362  lhop  19363  dvcvx  19367  ftc2ditglem  19392  itgsubstlem  19395  ig1pval  19558  elply2  19578  coeid2  19621  coemul  19633  taylthlem2  19753  ulmdvlem1  19777  mtest  19781  pserval2  19787  abelthlem1  19807  abelthlem3  19809  abelthlem8  19815  abelthlem9  19816  pige3  19885  0cxp  20013  leibpi  20238  mule1  20386  bposlem5  20527  lgsval3  20553  lgsdinn0  20579  dchrvmasumlem1  20644  dchrisum0flblem1  20657  rpvmasum2  20661  padicval  20766  grpoidinvlem4  20874  grposn  20882  grpoinvval  20892  grpodivval  20910  gxval  20925  gxnn0add  20941  subgoov  20972  ablosn  21014  ipval  21276  sspgval  21305  sspsval  21307  sspnval  21313  nmooval  21341  ipasslem1  21409  ipasslem4  21412  hial0  21681  hial02  21682  ocsh  21862  pjhval  21976  hosval  22320  homval  22321  hodval  22322  hfsval  22323  hfmval  22324  braval  22524  kbval  22534  eigvalval  22540  0hmop  22563  adj0  22574  lnopeq0i  22587  nmopcoi  22675  pjclem4  22779  pj3si  22787  hstoh  22812  strlem3a  22832  hstrlem3a  22840  mdexchi  22915  atcv0eq  22959  atcv1  22960  subfacp1lem3  23124  subfacp1lem5  23126  cvmlift2lem3  23247  vdgrval  23301  relexp1  23438  relexpcnv  23440  relexpadd  23446  altopthsn  23906  axsegconlem1  23956  ax5seglem9  23976  axpasch  23980  axeuclidlem  24001  axcontlem2  24004  bpolylem  24194  valpr  24570  1ded  25150  isfuna  25246  fnetr  25698  reftr  25701  fnejoin2  25730  isbnd3  25920  bndss  25922  ghomco  25985  pw2f1ocnv  26542  hbtlem7  26741  f1omvdco2  26803  pmtrfinv  26814  dvconstbi  26963  expgrowth  26964  addrfv  27086  subrfv  27087  mulvfv  27088  bnj1128  28393  lkrval  28651  pmapval  29319  polvalN  29467  watvalN  29555  ldilset  29671  ltrnset  29680  dilsetN  29715  trnsetN  29718  trlset  29723  trlval  29724  cdleme16b  29841  cdleme31fv1  29953  cdlemg1idlemN  30134  tgrpset  30307  tendoset  30321  erngset  30362  erngplus  30365  erngmul  30368  erngset-rN  30370  erngplus-rN  30373  dvaset  30567  dvaplusg  30571  dvamulr  30574  dvavadd  30577  dvavsca  30579  diafval  30594  dvhset  30644  dvhmulr  30649  dvhvadd  30655  dvhvsca  30664  docafvalN  30685  djafvalN  30697  dibfval  30704  dicfval  30738  dihfval  30794  dihval  30795  dihvalc  30796  dihvalb  30800  dochfval  30913  djhfval  30960  lcdval  31152  mapdfval  31190  mapdn0  31232  hvmapfval  31322  hdmap1fval  31360  hdmapfval  31393  hgmapfval  31452
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