Theorem sylan9eq 1519

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 1499	1 |- ((ph /\ ps) -> A = C)

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

This theorem is referenced by:  sylan9req 1520  sylan9eqr 1521  uneq12 2169  ineq12 2202  ifeq12 2358  ifbi 2361  prprc 2445  preq12b 2474  opeq12 2480  opthwiener 2796  relop 3265  xp11 3463  coi2 3497  funimass1 3558  f1orescnv 3689  fvopabn 3771  fvopab5 3778  rdgsucopab 3931  rdgsucopabn 3932  frsucopab 3939  abianfplem 3946  opreq12 3955  oprabval4g 4016  caoprmo 4056  eqop 4088  csbopeq1a 4096  oevn0 4138  oa0r 4157  om1r 4161  oe1m 4163  oarec 4180  omass 4195  oaabs 4236  map0 4328  sbthlem4 4430  sbthlem5 4431  mapenlem2 4470  mapdom2 4474  mapxpen 4475  xpmapenlem2 4477  xpmapenlem4 4479  xpmapenlem5 4480  mapunen 4482  phplem3 4490  phplem4 4491  opthreg 4576  addclprlem2 5091  mulclprlem 5093  reclem3pr 5130  mulcmpblnrlem 5154  supsrlem2 5198  addcnsr 5225  mulcnsr 5226  ax1id 5254  axcnre 5258  cnegextlem2 5318  cnegextlem3 5319  pnpcant 5450  add20 5576  recext 5657  nn0addclt 6067  uzindOLD 6156  om2uzran 6237  seq1lem1 6246  shftvalt 6283  abs00 6777  faclbnd4lem3 6887  bcval3tOLD 6896  bcval4t 6899  bcclt 6910  fsumconst 6976  serzrelem 6999  isumclimtf 7131  fsum0diaglem2 7192  ruclem4 7456  infxpidmlem4 7498  cldcls 7624  isopn3 7639  cnsscnp 7711  metxptval 7770  grpidinvlem4 7985  grpsn 8061  ablsn 8062  sspgval 8322  sspsval 8324  sspnval 8330  ipasslem1 8421  ipasslem4 8424  minveclem36 8511  hial0 8889  hial02 8890  ocsh 9072  hosvalt 9433  hosvaltOLD 9434  homvalt 9435  hodvalt 9436  hodvaltOLD 9437  hfsvalt 9438  hfmvalt 9439  bravalvalt 9784  kbvalvalt 9794  eigvalt 9800  0hmop 9823  adj0 9834  lnopeq0 9847  nmopco 9942  rnbra 9953  kbass2t 9962  hmopidmch 9990  pjclem4 10037  pj3s 10045  hstoht 10069  strlem3a 10089  hstrlem3a 10097  mdexch 10170  atcv0eq 10214  atcv1t 10215  1ded 10515

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain