Theorem sylan9eq 1948

Description: An equality transitivity deduction. (The proof was 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		eqtr 1904	. 2 |- ((A = B /\ B = C) -> A = C)
2		sylan9eq.1	. 2 |- (ph -> A = B)
3		sylan9eq.2	. 2 |- (ps -> B = C)
4	1, 2, 3	syl2an 503	1 |- ((ph /\ ps) -> A = C)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298

This theorem is referenced by:  sylan9req 1950  sylan9eqr 1951  difeq12 2721  uneq12 2750  ineq12 2791  ifeq12 2992  ifbi 2995  prprc 3110  preq12b 3154  opeq12 3160  opthwiener 3554  xpeq12 4020  relop 4113  xp11 4347  coi2 4414  funimass1 4491  f1orescnv 4655  resdif 4659  fvopabn 4749  fvopab5 4756  opreq12 4891  oprabval4g 4960  oprabval4gALT 4961  caoprmo 5003  eqopi 5043  csbopeq1a 5052  dfoprab5sf 5058  rdgsucopab 5154  rdgsucopabn 5155  frsucopab 5162  abianfplem 5170  oevn0 5199  oa0r 5220  om1r 5224  oe1m 5226  oarec 5244  omass 5259  oeoalem 5271  oeoa 5272  oeoe 5274  oaabs 5309  map0 5403  sbthlem4 5513  sbthlem5 5514  mapenlem2 5584  mapdom2 5588  mapxpen 5589  xpmapenlem2 5591  xpmapenlem4 5593  xpmapenlem5 5594  mapunen 5596  phplem3 5604  phplem4 5605  opthreg 5709  addclprlem2 6271  mulclprlem 6273  reclem3pr 6310  mulcmpblnrlem 6334  supsrlem2 6378  addcnsr 6405  mulcnsr 6406  ax1id 6435  axcnre 6439  cnegexlem2 6500  cnegexlem3 6501  pnpcan 6645  add20i 6782  recex 6876  nn0addcl 7329  uzindOLD 7420  om2uzrani 7711  seq1lem1 7722  shftval 7759  abs00i 8093  faclbnd4lem3 8202  bcval2 8211  bcval4 8213  bccl 8224  fsumconst 8298  serzrelem 8321  isumclimtfi 8456  fsum0diaglem2 8519  efieq1re 8751  ruclem4 8782  infxpidmlem4 8824  cldcls 8958  isopn3 8973  cnsscnp 9049  metxptval 9107  grpidinvlem4 9331  grpsn 9340  gxval 9381  gx1 9385  gxnn0add 9397  ablsn 9433  sspgval 9727  sspsval 9729  sspnval 9735  ipasslem1 9831  ipasslem4 9834  minveclem36 9925  hial0 10601  hial02 10602  ocsh 10789  hosval 11149  hosvalOLD 11150  homval 11151  hodval 11152  hodvalOLD 11153  hfsval 11154  hfmval 11155  bravalval 11505  kbvalval 11515  eigval1 11521  0hmop 11544  adj0 11556  lnopeq0i 11569  nmopcoi 11665  rnbra 11678  kbass2 11688  hmopidmchi 11723  pjclem4 11772  pj3si 11780  hstoh 11804  strlem3a 11824  hstrlem3a 11832  mdexchi 11907  atcv0eq 11951  atcv1 11952  bnj1128 13428  fz1eqblem 13608  dvdsnegb 13672  dvdscmul 13680  dvds2ln 13684  dvds2add 13685  dvds2sub 13686  gcdn0val 13717  eucalgf 13751  eucalginv 13752  eucalglt 13753  mulgcdlem2 13757  mulgcdlem5 13760  frsucopabn 13911  altopeq12 14089  seqzp2 14716  mamb 15030  1ded 15085  cnconn 15444  ufileu 15573  cnoprab1 15921  cnoprab2 15922  bndss 15942  heiborlem32 15986  bfp 16009  rrnmval 16014  ghomco 16040  reparpht 16065  pcoval 16073  pcoval1 16074  pcoval2 16075  pcohtpylem3 16082  pcorev 16087  ordintdif 16440  addrfv 16469  subrfv 16470  mulvfv 16471  lubval 16804  glbval 16809  joinval 16815  meetval 16822  grpidinvlem4NEW 17112  grpinvvalNEW 17126  plusssval 17205  ocvval 17207  pmapval 17237  polval 17318  watomval 17393  dilset 17402  trnset 17405

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain