Theorem syl6eq 1515

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 1499	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  syl6req 1516  syl6eqr 1517  3eqtr3g 1522  csbconstgf 2000  ssin 2222  un00 2296  preq12b 2474  intex 2719  intnex 2720  euuni 2871  rabsnt 2884  reuunisn 2885  sucprc 3034  onuninsuc 3098  dmsnop 3317  dmxpid 3322  elreldm 3327  relimasn 3409  xpnz 3452  xpdisj1 3454  xpdisj2 3455  resdisj 3457  dmxpss 3459  rnxpss 3460  unixp 3503  unixp0 3504  cnvresid 3555  funimacnv 3557  fconst 3643  f1o00 3699  fvprc 3706  funfv 3755  funfv2f 3757  fvopabn 3771  fopabcos 3818  fconst5 3833  tz7.44-2 3914  dfrdg2 3918  rdgval 3925  fnrnoprval 4021  1stval 4065  2ndval 4066  1st2val 4079  2nd2val 4080  om0 4140  oe0m 4141  oe0m0 4143  oe0 4145  oev2 4146  om0r 4158  oe1m 4163  oawordeulem 4172  oa00 4177  oarec 4180  oeworde 4204  nnmsucr 4224  oaabs 4236  nneob 4239  map0e 4326  en1 4407  fundmen 4409  mapsnen 4410  xpsnen 4415  xpcomen 4419  xpdom2 4422  sbthlem5 4431  sbthlem8 4434  fodomr 4463  mapdom2lem 4473  xpmapenlem2 4477  xpmapenlem4 4479  mapunen 4482  unifi 4532  fiint 4534  abfii3 4537  supsn 4563  inf3lema 4581  inf3lemd 4584  r1val1 4630  rankval2 4642  rankr1 4646  rankeq0 4668  rankxplim3 4686  scott0 4689  aceq5lem3 4709  kmlem2 4738  kmlem11 4747  numthlem 4755  zorn2lem1 4760  cardval 4798  cardaleph 4857  cardcf 4883  cfeq0 4886  cfom 4888  recmulpq 5042  genpv 5074  genpass 5084  addcompr 5095  mulcompr 5097  mulcmpblnrlem 5154  recexsrlem 5184  ssgt0sr 5189  addresr 5228  mulresr 5229  ax1id 5254  axcnre 5258  addcan 5323  negeu 5327  1re 5407  add20 5576  recextlem2 5656  mulcan 5659  mul0or 5663  receu 5670  nn0addclt 6067  nn0mulcl 6069  znegclt 6110  elnn0nn 6118  zltp1let 6128  nneo 6144  dfuz 6150  uzindOLD 6156  nn0ind-raph 6162  seq1lem1 6246  seq1suclem 6253  ndmioo 6307  seqz1 6479  exp0t 6503  1expt 6516  mulexpt 6525  recexpt 6526  exple1t 6538  sumsqne0 6565  sq0i 6567  bernneq 6583  discrlem3 6588  crne0 6670  crrecz 6672  reim0bt 6712  rereb 6715  abs00 6777  abs1m 6841  cau2 6850  facp1t 6873  faclbnd3 6884  faclbnd4lem1 6885  faclbnd4lem3 6887  faclbnd4lem4 6888  bcpasc 6907  dffsum 6936  csbfsumlem 6964  fsumrev 6967  fsumconst 6976  ser1ser0 6986  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem6 7009  binom 7010  climconst 7031  caucvg3t 7104  ser1clim0 7109  cvgcmp3cetlem1 7124  dfisum 7127  isumshft 7139  isumshft2 7140  georeclim 7175  geoisumr 7178  fsum0diag 7193  mulc1cncf 7214  ivthlem8 7223  ivthlem8OLD 7232  dfef2 7249  ef0lem 7252  efseq0ex 7253  efaddlem6 7285  efcant 7310  ef1tllem 7323  efgt0 7345  sincossqt 7403  absefit 7424  demoivre 7426  acdc3 7429  acdc2lem2 7431  acdc2 7432  acdc5lem2 7434  acdc5 7435  acdc 7437  xpnnen 7441  infxpidmlem4 7498  infxpidmlem8 7502  infxpidmlem10 7504  alephadd 7524  tgval2t 7559  subtop 7588  indistop 7590  fctop 7592  cctop 7594  idcn 7705  cncnplem4 7716  metssba2 7749  metreslem 7762  metres 7763  metxptval 7770  blfval2 7776  cncfmet 7844  dscmet 7856  iscau 7874  xplm 7909  grpsn 8061  ringsn 8100  vcoprne 8136  nvvcop 8151  bafval 8161  ipid 8297  iporthcom 8303  ip0r 8304  ip0l 8305  nmo0 8383  nmlno0lem 8385  nmlnoubi 8388  ipasslem2 8422  pythi 8441  siilem1 8442  siii 8444  ubthlem8 8467  minveclem19 8494  minveclem27 8502  sincosq1eq 8626  efifolem2 8638  efifolem7 8643  efif1lem5 8649  circcltOLD 8656  circgrpOLD 8658  efper 8669  hvmul0t 8814  hvsubidt 8816  hvaddsubvalt 8823  hvsubeq0 8851  hvsub0t 8864  hi02t 8884  orthcom 8895  bcseq 8907  normgt0tOLD 8914  normgt0t 8915  normpyth 8930  hlim0 9026  hsn0elch 9041  ocsh 9072  occllem7 9095  omlsilem 9159  pjoc1 9179  shjcomt 9245  shs00 9288  chj00 9325  h1de2b 9392  h1de2bOLD 9393  h1datom 9421  fh1t 9478  fh2t 9479  cm2jt 9480  nonbool 9513  pjssge0 9544  hosubeq0 9669  eigre 9677  eigorth 9680  kbpjt 9796  0cnop 9819  0cnfn 9820  0lnfn 9825  nmop0 9826  nmfn0 9827  nmop0h 9831  nmlnop0ALT 9835  lnopco0 9844  lnopeq0 9847  nmcoplb 9873  nmophm 9876  lnopcon 9878  nmbdfnlb 9893  nmcfnlb 9902  lnfncon 9905  nlelsh 9908  nmopco 9942  unierr 9950  nmopleidt 9983  pjsdi2 9996  pjclem1 10033  hstnmoct 10060  hst1ht 10064  strlem3a 10089  strlem4 10091  golem1 10108  stcltrlem1 10113  mdsl1 10156  mdslmd3 10167  csmdsym 10169  atoml2 10218  atord 10219  atabs 10236  sumdmdlem2 10253  cdj3lem1 10266  ghomsn 10293  cayleylem3 10318  moec 10357  neiopne 10369  isfil 10433  oefil2 10441  eloi 10503  ismona 10579

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