Theorem sylan9eqr 1529

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

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

This theorem is referenced by:  csbie2t 2033  opprc3 2797  onuninsuc 3108  fun2ssres 3553  funssfv 3735  abianfplem 3961  caoprmo 4070  2ndconst 4097  eqop 4104  oev2 4162  oesuc 4166  oawordeulem 4188  om00 4206  omass 4211  nneob 4255  sbthlem4 4450  sbthlem6 4452  fodomr 4483  mapenlem1 4489  mapdom2 4494  mapunen 4502  ssenen 4504  r1val1 4658  rankonid 4695  unxpdomlem 4843  cardaleph 4885  ltexpq 5080  addclprlem1 5118  mulclprlem 5121  1idpr 5133  prlem934a 5137  prlem936a 5153  prlem936 5155  reclem3pr 5158  mulcmpblnrlem 5182  recexsrlem 5212  ssgt0sr 5217  ax1id 5282  negeu 5355  pncant 5397  receu 5701  infmsup 6068  nn0addclt 6120  flhalft 6246  qaddclt 6269  qmulclt 6271  qrecclt 6273  seq1shftid 6356  expcllem 6575  expne0it 6588  expge1t 6593  expmult 6597  discrlem3 6658  reim0bt 6775  cjexpt 6817  cau2 6913  fsumsplit 7020  fsumadd 7022  serz0 7053  climconst 7094  climsub 7130  ser1const 7171  expcnv 7233  geoser 7234  ef0lem 7310  0ntr 7702  metssba2 7810  grpidinvlem2 8049  grpsn 8124  nvz 8297  ipfval 8352  lnon0 8458  ipasslem2 8491  htthlem4 8623  sinper 8690  cosper 8691  efifolem6 8727  efper 8747  hiidge0t 8964  normgt0tOLD 8993  normgt0t 8994  hsn0elch 9120  shsel3t 9279  spansneleq 9493  normcant 9499  h1datom 9504  fh1t 9561  spansncv 9597  5oalem1 9599  3oalem2 9608  pjds 9657  kbpjt 9880  0hmop 9907  0lnfn 9909  adj0 9919  branmfnt 10038  hst1ht 10154  mdsl0 10237  superpos 10281  sumdmdlem 10345  cdj3lem1 10361  cnvtr 10638  1ded 10671  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain