Theorem sylan9eq 1525

Description: An equality transitivity deduction.

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	. . 3 |- (ph -> A = B)
2	1	adantr 389	. 2 |- ((ph /\ ps) -> A = B)
3		sylan9eq.2	. . 3 |- (ps -> B = C)
4	3	adantl 388	. 2 |- ((ph /\ ps) -> B = C)
5	2, 4	eqtrd 1505	1 |- ((ph /\ ps) -> A = C)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955

This theorem is referenced by:  sylan9req 1526  sylan9eqr 1527  uneq12 2176  ineq12 2209  ifeq12 2365  ifbi 2368  prprc 2451  preq12b 2480  opeq12 2486  opthwiener 2803  relop 3271  xp11 3472  coi2 3507  funimass1 3568  f1orescnv 3699  fvopabn 3781  fvopab5 3788  rdgsucopab 3941  rdgsucopabn 3942  frsucopab 3949  abianfplem 3956  opreq12 3965  oprabval4g 4026  caoprmo 4065  eqop 4097  csbopeq1a 4105  oevn0 4147  oa0r 4166  om1r 4170  oe1m 4172  oarec 4189  omass 4204  oaabs 4245  map0 4337  sbthlem4 4439  sbthlem5 4440  mapenlem2 4479  mapdom2 4483  mapxpen 4484  xpmapenlem2 4486  xpmapenlem4 4488  xpmapenlem5 4489  mapunen 4491  phplem3 4499  phplem4 4500  opthreg 4587  addclprlem2 5102  mulclprlem 5104  reclem3pr 5141  mulcmpblnrlem 5165  supsrlem2 5209  addcnsr 5236  mulcnsr 5237  ax1id 5265  axcnre 5269  cnegextlem2 5329  cnegextlem3 5330  pnpcant 5461  add20 5586  recext 5667  nn0addclt 6077  uzindOLD 6166  om2uzran 6250  seq1lem1 6259  shftvalt 6296  abs00 6792  faclbnd4lem3 6902  bcval3tOLD 6911  bcval4t 6914  bcclt 6925  fsumconst 6991  serzrelem 7014  isumclimtf 7148  fsum0diaglem2 7209  ruclem4 7473  infxpidmlem4 7515  cldcls 7642  isopn3 7657  cnsscnp 7732  metxptval 7792  grpidinvlem4 8013  grpsn 8088  ablsn 8089  sspgval 8350  sspsval 8352  sspnval 8358  ipasslem1 8449  ipasslem4 8452  minveclem36 8539  hial0 8923  hial02 8924  ocsh 9111  hosvalt 9473  hosvaltOLD 9474  homvalt 9475  hodvalt 9476  hodvaltOLD 9477  hfsvalt 9478  hfmvalt 9479  bravalvalt 9825  kbvalvalt 9835  eigvalt 9841  0hmop 9864  adj0 9875  lnopeq0 9888  nmopco 9984  rnbra 9996  kbass2t 10006  hmopidmch 10035  pjclem4 10083  pj3s 10091  hstoht 10115  strlem3a 10135  hstrlem3a 10143  mdexch 10218  atcv0eq 10262  atcv1t 10263  1ded 10587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1468

Copyright terms: Public domain