Theorem syl6eq 1523

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
syl6eq	|- (ph -> A = C)

Proof of Theorem syl6eq

Step	Hyp	Ref	Expression
1		syl6eq.1	. 2 |- (ph -> A = B)
2		syl6eq.2	. . 3 |- B = C
3	2	a1i 8	. 2 |- (ph -> B = C)
4	1, 3	eqtrd 1507	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  syl6req 1524  syl6eqr 1525  3eqtr3g 1530  csbconstgf 2010  ssin 2232  un00 2306  preq12b 2483  intex 2729  intnex 2730  euuni 2881  rabsnt 2894  reuunisn 2895  sucprc 3044  onuninsuc 3108  dmsnop 3328  dmxpid 3333  elreldm 3338  relimasn 3425  xpnz 3466  xpdisj1 3468  xpdisj2 3469  resdisj 3471  dmxpss 3473  rnxpss 3474  unixp 3517  unixp0 3518  cnvresid 3569  funimacnv 3571  fconst 3658  f1o00 3714  fvprc 3721  funfv 3770  funfv2f 3772  fvopabn 3786  fopabcos 3833  fconst5 3848  tz7.44-2 3929  dfrdg2 3933  rdgval 3940  fnrnoprval 4036  1stval 4081  2ndval 4082  1st2val 4095  2nd2val 4096  om0 4156  oe0m 4157  oe0m0 4159  oe0 4161  oev2 4162  om0r 4174  oe1m 4179  oawordeulem 4188  oa00 4193  oarec 4196  oeworde 4220  nnmsucr 4240  oaabs 4252  nneob 4255  map0e 4342  en1 4426  fundmen 4428  mapsnen 4429  xpsnen 4435  xpcomen 4439  xpdom2 4442  sbthlem5 4451  sbthlem8 4454  fodomr 4483  mapdom2lem 4493  xpmapenlem2 4497  xpmapenlem4 4499  mapunen 4502  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii3OLD 4563  supsn 4591  inf3lema 4609  inf3lemd 4612  r1val1 4658  rankval2 4670  rankr1 4674  rankeq0 4696  rankxplim3 4714  scott0 4717  aceq5lem3 4737  kmlem2 4766  kmlem11 4775  numthlem 4783  zorn2lem1 4788  cardval 4826  cardaleph 4885  cardcf 4911  cfeq0 4914  cfom 4916  recmulpq 5070  genpv 5102  genpass 5112  addcompr 5123  mulcompr 5125  mulcmpblnrlem 5182  recexsrlem 5212  ssgt0sr 5217  addresr 5256  mulresr 5257  ax1id 5282  axcnre 5286  addcan 5351  negeu 5355  1re 5435  add20 5602  recextlem2 5683  mulcan 5686  mulcanOLD 5687  mul0or 5694  receu 5701  nn0addclt 6120  nn0mulcl 6122  znegclt 6163  elnn0nn 6171  zltp1let 6181  nneo 6197  dfuz 6202  uzindOLD 6208  nn0ind-raph 6214  seq1lem1 6309  seq1suclem 6316  ndmioo 6370  eliooret 6386  seqz1 6547  exp0t 6571  1expt 6584  mulexpt 6594  recexpt 6595  exple1t 6607  sumsqne0 6634  sq0i 6636  bernneq 6652  discrlem3 6658  crne0 6739  crrecz 6741  reim0bt 6775  rerebt 6776  abs00 6842  abs1m 6904  cau2 6913  facp1t 6936  faclbnd3 6947  faclbnd4lem1 6948  faclbnd4lem3 6950  faclbnd4lem4 6951  bcpasc 6969  dffsum 6998  csbfsumlem 7026  fsumrev 7029  fsumconst 7038  ser1ser0 7048  binomlem1 7066  binomlem2 7067  binomlem3 7068  binomlem4 7069  binomlem6 7071  binom 7072  climconst 7094  caucvg3t 7168  ser1clim0 7173  cvgcmp3cetlem1 7188  dfisum 7191  isumshft 7204  isumshft2 7205  georeclim 7240  geoisumr 7243  fsum0diag 7258  mulc1cncf 7279  ivthlem8 7288  dfef2 7307  ef0lem 7310  efseq0ex 7311  efaddlem6 7343  efcant 7368  ef1tllem 7381  efgt0 7404  sincossqt 7461  absefit 7482  demoivre 7484  acdc3 7487  acdc2lem2 7489  acdc2 7490  acdc5lem2 7492  acdc5 7493  acdc 7495  xpnnen 7499  infxpidmlem4 7555  infxpidmlem8 7559  infxpidmlem10 7561  alephadd 7582  tgval2t 7617  subtop 7646  indistop 7648  fctopOLD 7650  cctop 7652  idcn 7766  cncnplem4 7777  metssba2 7810  metreslem 7822  metres 7823  metxptval 7830  blfval2 7836  cncfmet 7905  dscmet 7918  iscau 7936  xplm 7975  grpsn 8124  ringsn 8163  vcoprne 8198  nvvcop 8213  bafval 8223  ipid 8363  iporthcom 8369  ip0r 8370  ip0l 8371  nmo0 8451  nmlno0lem 8453  nmlnoubi 8456  ipasslem2 8491  pythi 8510  siilem1 8511  siii 8513  ubthlem8 8536  minveclem19 8563  minveclem27 8571  sinkpi 8697  sincosq1eq 8709  efifolem2 8723  efifolem7 8728  efif1lem5 8734  efper 8747  hvmul0t 8893  hvsubidt 8895  hvaddsubvalt 8902  hvsubeq0 8930  hvsub0t 8943  hi02t 8963  orthcom 8974  bcseq 8986  normgt0tOLD 8993  normgt0t 8994  normpyth 9009  hlim0 9105  hsn0elch 9120  ocsh 9156  occllem7 9179  omlsilem 9244  pjoc1 9264  shjcomt 9330  shs00 9373  chj00 9410  h1de2b 9477  h1datom 9504  fh1t 9561  fh2t 9562  cm2jt 9563  nonbool 9596  pjssge0 9627  hosubeq0 9752  eigre 9760  eigorth 9763  kbpjt 9880  0cnop 9903  0cnfn 9904  0lnfn 9909  nmop0 9910  nmfn0 9911  nmop0h 9916  nmlnop0ALT 9920  lnopco0 9929  lnopeq0 9932  nmcoplb 9958  nmophm 9961  lnopcon 9963  nmbdfnlb 9978  nmcfnlb 9987  lnfncon 9990  nlelsh 9993  adjeq0 10024  nmopco 10028  unierr 10037  nmopleidt 10072  pjsdi2 10085  pjclem1 10123  hstnmoct 10150  hst1ht 10154  strlem3a 10179  strlem4 10181  golem1 10198  stcltrlem1 10203  mdsl1 10248  mdslmd3 10259  csmdsym 10261  atoml2 10310  atord 10311  atabs 10328  sumdmdlem2 10346  cdj3lem1 10361  ghomsn 10388  cayleylem3 10411  moec 10461  neiopne 10474  eqindhome 10541  isfil 10558  oefil2 10567  eloi 10659  ismona 10737

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