Theorem syl6eq 1566

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

Syntax hints:   -> wi 3   = wceq 992

This theorem is referenced by:  syl6req 1567  syl6eqr 1568  3eqtr3g 1573  csbconstgf 2061  ssin 2284  un00 2359  preq12b 2548  intex 2803  intnex 2804  sucprc 3048  euuni 3105  rabsnt 3117  reuunisn 3118  onuninsuci 3194  dmxpid 3420  elreldm 3425  relimasn 3517  xpnz 3551  xpdisj1 3553  xpdisj2 3554  resdisj 3556  dmxpss 3558  rnxpss 3559  dmsnop 3577  unixp 3622  unixp0 3623  cnvresid 3674  funimacnv 3676  fconst 3765  f1o00 3825  fvprc 3832  funfv 3881  funfv2f 3883  fvopabn 3897  fopabcos 3947  fconst5 3962  fnrnoprv 4097  1stval 4142  2ndval 4143  1st2val 4158  2nd2val 4159  1stconst 4190  curry2 4196  fsplit 4204  tz7.44-2 4230  dfrdg2 4234  rdgval 4241  om0 4292  oe0m 4293  oe0m0 4295  oe0 4297  oev2 4298  om0r 4310  oe1m 4315  oawordeulem 4324  oa00 4329  oarec 4332  oeworde 4356  oeoa 4360  oeoelem 4361  oeoe 4362  nnmsucr 4380  oaabs 4392  nneob 4395  map0e 4483  en1 4567  fundmen 4569  mapsnen 4570  xpsnen 4576  xpcomen 4580  xpdom2 4583  sbthlem5 4596  sbthlem8 4599  fodomr 4628  mapdom2lem 4640  xpmapenlem2 4644  xpmapenlem4 4646  mapunen 4649  unifi 4701  fiint 4703  abfii3 4706  pwfi 4714  supsn 4734  inf3lema 4754  inf3lemd 4757  r1val1 4804  rankval2 4816  rankr1 4820  rankeq0 4842  rankxplim3 4860  scott0 4863  aceq5lem3 4883  kmlem2 4912  kmlem11 4921  numthlem 4929  zorn2lem1 4934  cardval 4973  cardaleph 5035  cardcf 5061  cfeq0 5064  cfom 5066  recmulpq 5224  genpv 5256  genpass 5266  addcompr 5277  mulcompr 5279  mulcmpblnrlem 5336  recexsrlem 5366  ssgt0sr 5371  addresr 5410  mulresr 5411  ax1id 5436  axcnre 5440  addcani 5505  negeui 5509  1re 5589  add20i 5756  recextlem2 5839  mulcani 5842  mul0ori 5846  receui 5853  nn0addcl 6288  nn0mulcli 6290  znegcl 6331  elnn0nn 6339  zltp1le 6349  nneoi 6368  dfuzi 6373  uzindOLD 6379  nn0ind-raph 6385  ndmioo 6496  elioore 6512  seq1lem1 6674  seq1suclem 6681  seqz1 6742  exp0 6766  1exp 6779  mulexp 6788  exprec 6789  exprecOLD 6790  exple1 6804  sumsqne0i 6831  sq0i 6833  bernneq 6849  bernneqOLD 6850  discrlem3 6859  crne0i 6940  crreczi 6942  reim0b 6976  rereb 6977  abs00i 7044  abs1mi 7107  cau2i 7116  facp1 7139  faclbnd3 7150  faclbnd4lem1 7151  faclbnd4lem3 7153  faclbnd4lem4 7154  bcpasci 7172  dffsum 7201  csbfsumlem 7229  fsumrev 7232  fsumconst 7241  ser1ser0i 7251  binomlem1 7269  binomlem2 7270  binomlem3 7271  binomlem4 7272  binomlem6 7274  binomi 7275  climconsti 7297  caucvg3 7371  ser1clim0 7376  cvgcmp3cetlem1 7392  dfisum 7395  isumshfti 7408  isumshft2i 7409  georeclim 7445  geoisumr 7448  fsum0diag 7463  mulc1cncf 7484  ivthlem8 7493  dfef2i 7512  ef0lem 7515  efseq0ex 7516  efaddlem6 7548  efcan 7573  ef1tllem 7586  efgt0i 7612  sincossq 7669  cos2tsin 7672  absefi 7691  demoivre 7695  acdc3 7698  acdc2lem2 7701  acdc2 7702  acdc5lem2 7704  acdc5 7705  acdc 7707  xpnnen 7711  infxpidmlem4 7767  infxpidmlem8 7771  infxpidmlem10 7773  alephadd 7794  tgval2 7829  subtop 7858  indistop 7860  cctop 7862  idcn 7976  cncnplem4 7987  metssba2 8020  metreslem 8032  metres 8033  metxptval 8040  blfval2 8046  cncfmet 8116  dscmet 8129  iscau 8147  xplm 8186  gid0 8271  grpsn 8273  grpidvallem 8274  grpidval 8275  gx0 8317  gxnn0neg 8319  gxnn0suc 8320  ringsn 8405  vcoprne 8445  nvvcop 8460  bafval 8470  ipid 8617  iporthcom 8623  ip0r 8624  ip0l 8625  nmo0 8706  nmlno0lem 8708  nmlnoubi 8711  ipasslem2 8747  pythi 8766  siilem1 8767  siii 8769  ubthlem8 8794  minveclem19 8823  minveclem27 8831  sincosq1eq 8977  sinkpi 8981  coskpi 8982  sineq0re 8985  efifolem2 8995  efifolem7 9000  efif1lem5 9006  efper 9019  hvmul0 9168  hvsubid 9170  hvaddsubval 9177  hvsubeq0i 9205  hvsub0 9219  hi02 9239  orthcom 9250  bcseqi 9262  normgt0OLD 9269  normgt0 9270  normpythi 9285  hlim0 9381  hsn0elch 9396  ocsh 9432  occllem7 9455  omlsilem 9520  pjoc1i 9540  shjcom 9606  shs00i 9649  chj00i 9686  h1de2bi 9753  h1datomi 9780  fh1 9837  fh2 9838  cm2j 9839  nonbooli 9874  pjssge0ii 9905  hosubeq0i 10032  eigrei 10040  eigorthi 10043  kbpj 10160  0cnop 10182  0cnfn 10183  0lnfn 10188  nmop0 10189  nmfn0 10190  nmop0h 10195  nmlnop0iALT 10199  lnopco0i 10208  lnopeq0i 10211  nmcoplbi 10237  nmophmi 10240  lnopconi 10242  nmbdfnlbi 10257  nmcfnlbi 10266  lnfnconi 10269  nlelshi 10272  adjeq0 10303  nmopcoi 10307  unierri 10316  nmopleid 10352  pjsdi2i 10365  pjclem1 10404  hstnmoc 10431  hst1h 10435  strlem3a 10460  strlem4 10462  golem1 10479  stcltrlem1 10484  mdsl1i 10529  mdslmd3i 10540  csmdsymi 10542  atoml2i 10592  atordi 10593  atabsi 10610  sumdmdlem2 10628  cdj3lem1 10643  ghomsn 10673  cayleylem3 10696  moec 10745  neiopne 10757  fldsqcp2 10780  fldsqcp 10781  scprefat2 10784  eloi 10817  rnplrnml3 10950  on1el3 10962  zrdivrng 10969  eqindhome 11047  oefil2 11079  clindistop 11131  topsinind 11136  singcon 11137  ismona 11264  elfiun 11421  fictb 11423  finsschain 11425  ordtypelem1 11427  ordtypelem6 11432  omsublim 11448  topbnd 11460  subcld 11480  cnsubsp2 11484  compsublem 11487  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  connsub 11502  cnconn 11503  reconnlem1 11507  ivthALT 11515  2ndcctbss 11539  comppfsc 11578  fsubbas 11630  filrn 11643  ufileu 11658  filufint 11659  filcon 11665  flimcls 11684  flimfnfcls 11727  filnetlem5 11767  filnet 11768  gaid 11776  xp1st 11796  xp2nd 11797  upxp 11822  sdc 11877  mettrifi2 11913  txcnopab 11980  txsubsp 11983  txcld 11985  bndss 11998  blbnd 11999  totbndbnd 12000  heiborlem8 12018  heiborlem9 12019  heiborlem11 12021  heiborlem13 12023  heiborlem32 12042  bfplem11 12064  rrndm 12071  ismrer1 12080  phtpycom 12092  phtpycolem2 12094

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain