HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem sylan9eqr 1521
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
StepHypRef Expression
1 sylan9eqr.1 . . 3 |- (ph -> A = B)
2 sylan9eqr.2 . . 3 |- (ps -> B = C)
31, 2sylan9eq 1519 . 2 |- ((ph /\ ps) -> A = C)
43ancoms 436 1 |- ((ps /\ ph) -> A = C)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223   = wceq 953
This theorem is referenced by:  csbie2t 2023  opprc3 2787  onuninsuc 3098  fun2ssres 3539  funssfv 3720  abianfplem 3946  caoprmo 4056  2ndconst 4081  eqop 4088  oev2 4146  oesuc 4150  oawordeulem 4172  om00 4190  omass 4195  nneob 4239  sbthlem4 4430  sbthlem6 4432  fodomr 4463  mapenlem1 4469  mapdom2 4474  mapunen 4482  ssenen 4484  r1val1 4630  rankonid 4667  unxpdomlem 4815  cardaleph 4857  ltexpq 5052  addclprlem1 5090  mulclprlem 5093  1idpr 5105  prlem934a 5109  prlem936a 5125  prlem936 5127  reclem3pr 5130  mulcmpblnrlem 5154  recexsrlem 5184  ssgt0sr 5189  ax1id 5254  negeu 5327  pncant 5369  receu 5670  infmsup 6015  nn0addclt 6067  flhalft 6189  qaddclt 6207  qmulclt 6209  qrecclt 6211  seq1shftid 6293  expcllem 6507  expne0it 6519  expge1t 6524  expmult 6528  discrlem3 6588  reim0bt 6712  cjexpt 6752  cau2 6850  fsumsplit 6958  fsumadd 6960  serz0 6991  climconst 7031  climsub 7066  ser1const 7107  expcnv 7168  geoser 7169  ef0lem 7252  0ntr 7644  metssba2 7749  grpidinvlem2 7983  grpsn 8061  nvz 8236  ipfval 8286  ipasslem2 8422  htthlem4 8553  sinper 8609  cosper 8610  efifolem6 8642  efper 8669  hiidge0t 8885  normgt0tOLD 8914  normgt0t 8915  hsn0elch 9041  shsel3t 9194  spansneleq 9409  spansneleqOLD 9410  normcant 9416  h1datom 9421  fh1t 9478  spansncv 9514  5oalem1 9516  3oalem2 9525  pjds 9574  kbpjt 9796  0hmop 9823  0lnfn 9825  adj0 9834  branmfnt 9951  hst1ht 10064  mdsl0 10145  superpos 10189  sumdmdlem 10252  cdj3lem1 10266  cnvtr 10482  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