Theorem sylan9eqr 1951

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 1948	. 2 |- ((ph /\ ps) -> A = C)
4	3	ancoms 484	1 |- ((ps /\ ph) -> A = C)

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

This theorem is referenced by:  csbie2t 2578  opprc3 3543  onuninsuci 3921  fun2ssres 4461  fcoi1 4584  fcoi2 4586  funssfv 4692  fvopab6 4757  caoprmo 5003  eqop 5044  dfoprab5sf 5058  2ndconst 5071  iunfoprab 5072  abianfplem 5170  oev2 5207  oesuc 5211  oawordeulem 5236  om00 5254  omass 5259  oeoa 5272  oeoe 5274  nneob 5312  sbthlem4 5513  sbthlem6 5515  fodomr 5547  mapenlem1 5583  mapdom2 5588  mapunen 5596  ssenen 5598  r1val1 5769  rankonid 5806  unxpdomlem 5995  cardaleph 6033  ltexpq 6232  addclprlem1 6270  mulclprlem 6273  1idpr 6285  prlem934a 6289  prlem936a 6305  prlem936 6307  reclem3pr 6310  mulcmpblnrlem 6334  recexsrlem 6364  ssgt0sr 6369  ax1id 6435  negeui 6510  pncan 6557  receui 6890  infmsup 7277  nn0addcl 7329  qaddcl 7449  qmulcl 7451  qreccl 7453  flhalf 7487  cardfz 7719  seq1shftid 7769  expcllem 7818  expne0i 7830  expge1 7835  expmul 7840  discrlem3 7908  reim0b 8025  cjexp 8067  cau2i 8165  fsumsplit 8280  fsumadd 8282  serz0 8313  climconsti 8354  climsub 8390  ser1consti 8431  expcnv 8494  geoseri 8496  ef0lem 8572  indistop 8918  0ntr 8978  metssba2 9087  grpidinvlem2 9329  grpsn 9340  gxnn0neg 9386  gxid 9396  nvz 9629  ipfval 9691  lnon0 9798  ipasslem2 9832  htthlem4 9970  sinper 10039  cosper 10040  efifolem6 10081  efper 10101  extbas2 10292  hiidge0 10597  normgt0OLD 10626  normgt0 10627  hsn0elch 10753  shsel3 10912  spansneleq 11126  normcan 11132  h1datomi 11137  fh1 11194  spansncvi 11232  5oalem1 11234  3oalem2 11243  pjdsi 11292  kbpj 11517  0hmop 11544  0lnfn 11546  adj0 11556  branmfn 11675  branmfnOLD 11676  opsqrlem1 11711  hst1h 11799  mdsl0 11882  superpos 11926  sumdmdlem 11990  cdj3lem1 12006  dvdsnegb 13672  gcddvds 13722  gcdcl 13724  gcdabs 13737  coprmdvds 13783  cnvtr 15016  1ded 15085  dualcat2 15133  idfisf 15189  divexp 15779  geomcau 15849  lincmb01icc 15879  phtpycolem4 16054  pi1gp 16095  glbcon 17028  atltcvr 17072  grpidinvlem2NEW 17110  pmodlem2 17308  pmapjat 17314  osumcl 17375

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