Theorem sylan9eqr 1526

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
sylan9eqr.1	|- (ph -> A = B)
sylan9eqr.2	|- (ps -> B = C)

Assertion

Ref	Expression
sylan9eqr	|- ((ps /\ ph) -> A = C)

Proof of Theorem sylan9eqr

Step	Hyp	Ref	Expression
1		sylan9eqr.1	. . 3 |- (ph -> A = B)
2		sylan9eqr.2	. . 3 |- (ps -> B = C)
3	1, 2	sylan9eq 1524	. 2 |- ((ph /\ ps) -> A = C)
4	3	ancoms 436	1 |- ((ps /\ ph) -> A = C)

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

This theorem is referenced by:  csbie2t 2029  opprc3 2792  onuninsuc 3103  fun2ssres 3545  funssfv 3726  abianfplem 3952  caoprmo 4062  2ndconst 4087  eqop 4094  oev2 4152  oesuc 4156  oawordeulem 4178  om00 4196  omass 4201  nneob 4245  sbthlem4 4436  sbthlem6 4438  fodomr 4469  mapenlem1 4475  mapdom2 4480  mapunen 4488  ssenen 4490  r1val1 4638  rankonid 4675  unxpdomlem 4823  cardaleph 4865  ltexpq 5060  addclprlem1 5098  mulclprlem 5101  1idpr 5113  prlem934a 5117  prlem936a 5133  prlem936 5135  reclem3pr 5138  mulcmpblnrlem 5162  recexsrlem 5192  ssgt0sr 5197  ax1id 5262  negeu 5335  pncant 5377  receu 5678  infmsup 6023  nn0addclt 6075  flhalft 6197  qaddclt 6215  qmulclt 6217  qrecclt 6219  seq1shftid 6301  expcllem 6515  expne0it 6527  expge1t 6532  expmult 6536  discrlem3 6596  reim0bt 6720  cjexpt 6760  cau2 6858  fsumsplit 6966  fsumadd 6968  serz0 6999  climconst 7039  climsub 7074  ser1const 7115  expcnv 7176  geoser 7177  ef0lem 7260  0ntr 7652  metssba2 7760  grpidinvlem2 7999  grpsn 8076  nvz 8249  ipfval 8299  ipasslem2 8435  htthlem4 8566  sinper 8628  cosper 8629  efifolem6 8661  efper 8686  hiidge0t 8903  normgt0tOLD 8932  normgt0t 8933  hsn0elch 9059  shsel3t 9217  spansneleq 9432  spansneleqOLD 9433  normcant 9439  h1datom 9444  fh1t 9501  spansncv 9537  5oalem1 9539  3oalem2 9548  pjds 9597  kbpjt 9819  0hmop 9846  0lnfn 9848  adj0 9857  branmfnt 9976  hst1ht 10092  mdsl0 10174  superpos 10218  sumdmdlem 10281  cdj3lem1 10295  cnvtr 10518  1ded 10551

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

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

Copyright terms: Public domain