Theorem sylan9eq 2456

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

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 |- ( ph -> A = B )
2		sylan9eq.2	. 2 |- ( ps -> B = C )
3		eqtr 2421	. 2 |- ( ( A = B /\ B = C ) -> A = C )
4	1, 2, 3	syl2an 464	1 |- ( ( ph /\ ps ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649

This theorem is referenced by:  sylan9req  2457  sylan9eqr  2458  difeq12  3420  uneq12  3456  ineq12  3497  ifeq12  3712  ifbi  3716  preq12  3845  prprc  3876  preq12b  3934  opeq12  3946  opthwiener  4418  ordintdif  4590  xpeq12  4856  sosn  4906  nfimad  5171  coi2  5345  funimass1  5485  f1orescnv  5649  resdif  5655  fvmpt2  5771  fvmptnf  5781  oveq12  6049  cbvmpt2v  6111  ovmpt2g  6167  caofinvl  6290  eqopi  6342  fmpt2co  6389  rdgsucmptf  6645  frsucmpt  6654  abianfplem  6674  oevn0  6718  oa0r  6741  om1r  6745  oe1m  6747  omass  6782  oeoalem  6798  oeoa  6799  oeoe  6801  map0g  7012  xpcomco  7157  sbthlem4  7179  sbthlem5  7180  xpmapenlem  7233  phplem3  7247  phplem4  7248  unxpdomlem3  7274  ordtypelem7  7449  cardennn  7826  dfac9  7972  cdaassen  8018  alephsing  8112  axcc3  8274  ac6num  8315  konigthlem  8399  canthp1lem2  8484  ordpipq  8775  ltrnq  8812  addclprlem2  8850  mulclprlem  8852  prlem934  8866  prlem936  8880  mulcmpblnrlem  8904  addcnsr  8966  mulcnsr  8967  axcnre  8995  recex  9610  uzindOLD  10320  rpnnen1lem3  10558  rpnnen1lem5  10560  xaddpnf1  10768  xaddpnf2  10769  xaddmnf1  10770  xaddmnf2  10771  rexadd  10774  xaddnemnf  10776  xaddnepnf  10777  xadddilem  10829  om2uzrani  11247  om2uzrdg  11251  seqf1olem2  11318  seqf1o  11319  modexp  11469  faclbnd4lem3  11541  hashunsng  11620  swrdfv  11726  revfv  11750  shftcan1  11853  remul2  11890  immul2  11897  sumss  12473  geomulcvg  12608  ef0lem  12636  efieq1re  12755  rpnnen2lem1  12769  ruclem3  12787  dvdsnegb  12822  dvdscmul  12831  dvds2ln  12835  dvds2add  12836  dvds2sub  12837  gcdn0val  12965  rpmulgcd  13010  odzval  13132  pcval  13173  pcmpt  13216  prmreclem4  13242  1arithlem2  13247  vdwlem8  13311  ramcl2lem  13332  ramtcl  13333  ramtub  13335  ramcl2  13339  ramcl  13352  setsval  13448  prfcl  14255  curf1cl  14280  curfcl  14284  hofcl  14311  yonedalem4c  14329  lubval  14391  glbval  14396  joinval  14400  meetval  14407  psssdm  14603  grplactval  14841  cntzval  15075  odlem2  15132  gexlem2  15171  lsmvalx  15228  efgtval  15310  efgredlema  15327  vrgpval  15354  cyggex  15462  gsumcom2  15504  dvdsrtr  15712  abvtrivd  15883  lmhmco  16074  reslmhm  16083  lvecinv  16140  mplmon2  16508  subrgasclcl  16514  coe1fv  16559  zrhmulg  16746  znzrhval  16782  ocvval  16849  isopn3  17085  cnpval  17254  ptbasfi  17566  dfac14  17603  cnmptkk  17668  xkofvcn  17669  cnmptk1p  17670  cnmptk2  17671  xkocnv  17799  flfval  17975  ptcmplem3  18038  ptcmpg  18041  tmdmulg  18075  prdsxmslem2  18512  subgnm2  18628  nmoval  18702  fsum2cn  18854  pcovalg  18990  cphnm  19109  tchnmval  19140  ovolctb  19339  ioorcl  19422  uniioombllem2  19428  itg1addlem3  19543  itg1climres  19559  itg2uba  19588  itg2splitlem  19593  elcpn  19773  dvexp  19792  dvexp2  19793  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  dvlip2  19832  dveq0  19837  dv11cn  19838  lhop1lem  19850  lhop2  19852  lhop  19853  dvcvx  19857  ftc2ditglem  19882  itgsubstlem  19885  ig1pval  20048  elply2  20068  coeid2  20111  coemul  20123  taylthlem2  20243  ulmdvlem1  20269  mtest  20273  pserval2  20280  abelthlem1  20300  abelthlem3  20302  abelthlem8  20308  abelthlem9  20309  pige3  20378  0cxp  20510  leibpi  20735  mule1  20884  bposlem5  21025  lgsval3  21051  lgsdinn0  21077  dchrvmasumlem1  21142  dchrisum0flblem1  21155  rpvmasum2  21159  padicval  21264  nbgraop  21389  nbgraop1  21390  constr1trl  21541  1pthon  21544  2pthlem2  21549  constr3pthlem3  21597  vdgrval  21620  grpoidinvlem4  21748  grposn  21756  grpoinvval  21766  grpodivval  21784  gxval  21799  gxnn0add  21815  subgoov  21846  ablosn  21888  ipval  22152  sspgval  22181  sspsval  22183  sspnval  22189  nmooval  22217  ipasslem1  22285  ipasslem4  22288  hial0  22557  hial02  22558  ocsh  22738  pjhval  22852  hosval  23196  homval  23197  hodval  23198  hfsval  23199  hfmval  23200  braval  23400  kbval  23410  eigvalval  23416  0hmop  23439  adj0  23450  lnopeq0i  23463  nmopcoi  23551  pjclem4  23655  pj3si  23663  hstoh  23688  strlem3a  23708  hstrlem3a  23716  mdexchi  23791  atcv0eq  23835  atcv1  23836  measxun2  24517  measdivcstOLD  24531  measdivcst  24532  ballotlemfp1  24702  igamgam  24786  subfacp1lem3  24821  subfacp1lem5  24823  cvmlift2lem3  24945  relexp1  25084  relexpcnv  25086  relexpadd  25091  fprodss  25227  altopthsn  25710  axsegconlem1  25760  ax5seglem9  25780  axpasch  25784  axeuclidlem  25805  axcontlem2  25808  bpolylem  25998  mblfinlem  26143  mblfinlem2  26144  mbfresfi  26152  itg2addnclem  26155  itg2addnc  26158  fnetr  26256  reftr  26259  fnejoin2  26288  isbnd3  26383  bndss  26385  ghomco  26448  pw2f1ocnv  26998  hbtlem7  27197  f1omvdco2  27259  pmtrfinv  27270  dvconstbi  27419  expgrowth  27420  addrfv  27541  subrfv  27542  mulvfv  27543  refsum2cnlem1  27575  afveu  27884  el2spthonot0  28068  bnj1128  29065  lkrval  29571  pmapval  30239  polvalN  30387  watvalN  30475  ldilset  30591  ltrnset  30600  dilsetN  30635  trnsetN  30638  trlset  30643  trlval  30644  cdleme16b  30761  cdleme31fv1  30873  cdlemg1idlemN  31054  tgrpset  31227  tendoset  31241  erngset  31282  erngplus  31285  erngmul  31288  erngset-rN  31290  erngplus-rN  31293  dvaset  31487  dvaplusg  31491  dvamulr  31494  dvavadd  31497  dvavsca  31499  diafval  31514  dvhset  31564  dvhmulr  31569  dvhvadd  31575  dvhvsca  31584  docafvalN  31605  djafvalN  31617  dibfval  31624  dicfval  31658  dihfval  31714  dihval  31715  dihvalc  31716  dihvalb  31720  dochfval  31833  djhfval  31880  lcdval  32072  mapdfval  32110  mapdn0  32152  hvmapfval  32242  hdmap1fval  32280  hdmapfval  32313  hgmapfval  32372

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397