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

Theorem sylan9eq 2488
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 2453 . 2  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
41, 2, 3syl2an 464 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652
This theorem is referenced by:  sylan9req  2489  sylan9eqr  2490  difeq12  3460  uneq12  3496  ineq12  3537  ifeq12  3752  ifbi  3756  preq12  3885  prprc  3916  preq12b  3974  opeq12  3986  opthwiener  4458  ordintdif  4630  xpeq12  4897  sosn  4947  nfimad  5212  coi2  5386  funimass1  5526  f1orescnv  5690  resdif  5696  fvmpt2  5812  fvmptnf  5822  oveq12  6090  cbvmpt2v  6152  ovmpt2g  6208  caofinvl  6331  eqopi  6383  fmpt2co  6430  rdgsucmptf  6686  frsucmpt  6695  abianfplem  6715  oevn0  6759  oa0r  6782  om1r  6786  oe1m  6788  omass  6823  oeoalem  6839  oeoa  6840  oeoe  6842  map0g  7053  xpcomco  7198  sbthlem4  7220  sbthlem5  7221  xpmapenlem  7274  phplem3  7288  phplem4  7289  unxpdomlem3  7315  ordtypelem7  7493  cardennn  7870  dfac9  8016  cdaassen  8062  alephsing  8156  axcc3  8318  ac6num  8359  konigthlem  8443  canthp1lem2  8528  ordpipq  8819  ltrnq  8856  addclprlem2  8894  mulclprlem  8896  prlem934  8910  prlem936  8924  mulcmpblnrlem  8948  addcnsr  9010  mulcnsr  9011  axcnre  9039  recex  9654  uzindOLD  10364  rpnnen1lem3  10602  rpnnen1lem5  10604  xaddpnf1  10812  xaddpnf2  10813  xaddmnf1  10814  xaddmnf2  10815  rexadd  10818  xaddnemnf  10820  xaddnepnf  10821  xadddilem  10873  om2uzrani  11292  om2uzrdg  11296  seqf1olem2  11363  seqf1o  11364  modexp  11514  faclbnd4lem3  11586  hashunsng  11665  swrdfv  11771  revfv  11795  shftcan1  11898  remul2  11935  immul2  11942  sumss  12518  geomulcvg  12653  ef0lem  12681  efieq1re  12800  rpnnen2lem1  12814  ruclem3  12832  dvdsnegb  12867  dvdscmul  12876  dvds2ln  12880  dvds2add  12881  dvds2sub  12882  gcdn0val  13010  rpmulgcd  13055  odzval  13177  pcval  13218  pcmpt  13261  prmreclem4  13287  1arithlem2  13292  vdwlem8  13356  ramcl2lem  13377  ramtcl  13378  ramtub  13380  ramcl2  13384  ramcl  13397  setsval  13493  prfcl  14300  curf1cl  14325  curfcl  14329  hofcl  14356  yonedalem4c  14374  lubval  14436  glbval  14441  joinval  14445  meetval  14452  psssdm  14648  grplactval  14886  cntzval  15120  odlem2  15177  gexlem2  15216  lsmvalx  15273  efgtval  15355  efgredlema  15372  vrgpval  15399  cyggex  15507  gsumcom2  15549  dvdsrtr  15757  abvtrivd  15928  lmhmco  16119  reslmhm  16128  lvecinv  16185  mplmon2  16553  subrgasclcl  16559  coe1fv  16604  zrhmulg  16791  znzrhval  16827  ocvval  16894  isopn3  17130  cnpval  17300  ptbasfi  17613  dfac14  17650  cnmptkk  17715  xkofvcn  17716  cnmptk1p  17717  cnmptk2  17718  xkocnv  17846  flfval  18022  ptcmplem3  18085  ptcmpg  18088  tmdmulg  18122  prdsxmslem2  18559  subgnm2  18675  nmoval  18749  fsum2cn  18901  pcovalg  19037  cphnm  19156  tchnmval  19187  ovolctb  19386  ioorcl  19469  uniioombllem2  19475  itg1addlem3  19590  itg1climres  19606  itg2uba  19635  itg2splitlem  19640  elcpn  19820  dvexp  19839  dvexp2  19840  rolle  19874  cmvth  19875  mvth  19876  dvlip  19877  dvlipcn  19878  dvlip2  19879  dveq0  19884  dv11cn  19885  lhop1lem  19897  lhop2  19899  lhop  19900  dvcvx  19904  ftc2ditglem  19929  itgsubstlem  19932  ig1pval  20095  elply2  20115  coeid2  20158  coemul  20170  taylthlem2  20290  ulmdvlem1  20316  mtest  20320  pserval2  20327  abelthlem1  20347  abelthlem3  20349  abelthlem8  20355  abelthlem9  20356  pige3  20425  0cxp  20557  leibpi  20782  mule1  20931  bposlem5  21072  lgsval3  21098  lgsdinn0  21124  dchrvmasumlem1  21189  dchrisum0flblem1  21202  rpvmasum2  21206  padicval  21311  nbgraop  21436  nbgraop1  21437  constr1trl  21588  1pthon  21591  2pthlem2  21596  constr3pthlem3  21644  vdgrval  21667  grpoidinvlem4  21795  grposn  21803  grpoinvval  21813  grpodivval  21831  gxval  21846  gxnn0add  21862  subgoov  21893  ablosn  21935  ipval  22199  sspgval  22228  sspsval  22230  sspnval  22236  nmooval  22264  ipasslem1  22332  ipasslem4  22335  hial0  22604  hial02  22605  ocsh  22785  pjhval  22899  hosval  23243  homval  23244  hodval  23245  hfsval  23246  hfmval  23247  braval  23447  kbval  23457  eigvalval  23463  0hmop  23486  adj0  23497  lnopeq0i  23510  nmopcoi  23598  pjclem4  23702  pj3si  23710  hstoh  23735  strlem3a  23755  hstrlem3a  23763  mdexchi  23838  atcv0eq  23882  atcv1  23883  measxun2  24564  measdivcstOLD  24578  measdivcst  24579  ballotlemfp1  24749  igamgam  24833  subfacp1lem3  24868  subfacp1lem5  24870  cvmlift2lem3  24992  relexp1  25131  relexpcnv  25133  relexpadd  25138  fprodss  25274  binomfallfaclem2  25356  wrecseq123  25532  altopthsn  25806  axsegconlem1  25856  ax5seglem9  25876  axpasch  25880  axeuclidlem  25901  axcontlem2  25904  bpolylem  26094  mblfinlem2  26244  mblfinlem3  26245  mbfresfi  26253  itg2addnclem  26256  itg2addnc  26259  ftc1anclem2  26281  ftc1anclem5  26284  fnetr  26366  reftr  26369  fnejoin2  26398  isbnd3  26493  bndss  26495  ghomco  26558  pw2f1ocnv  27108  hbtlem7  27306  f1omvdco2  27368  pmtrfinv  27379  dvconstbi  27528  expgrowth  27529  addrfv  27650  subrfv  27651  mulvfv  27652  refsum2cnlem1  27684  afveu  27993  swrdccat3a0  28203  swrdccat  28216  lswrd1  28262  el2spthonot0  28338  bnj1128  29359  lkrval  29886  pmapval  30554  polvalN  30702  watvalN  30790  ldilset  30906  ltrnset  30915  dilsetN  30950  trnsetN  30953  trlset  30958  trlval  30959  cdleme16b  31076  cdleme31fv1  31188  cdlemg1idlemN  31369  tgrpset  31542  tendoset  31556  erngset  31597  erngplus  31600  erngmul  31603  erngset-rN  31605  erngplus-rN  31608  dvaset  31802  dvaplusg  31806  dvamulr  31809  dvavadd  31812  dvavsca  31814  diafval  31829  dvhset  31879  dvhmulr  31884  dvhvadd  31890  dvhvsca  31899  docafvalN  31920  djafvalN  31932  dibfval  31939  dicfval  31973  dihfval  32029  dihval  32030  dihvalc  32031  dihvalb  32035  dochfval  32148  djhfval  32195  lcdval  32387  mapdfval  32425  mapdn0  32467  hvmapfval  32557  hdmap1fval  32595  hdmapfval  32628  hgmapfval  32687
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator