Theorem syl6eq 1944

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

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  syl6req 1945  syl6eqr 1946  3eqtr3g 1952  3eqtr4a 1954  csbconstgf 2551  ssinOLD 2815  un00 2907  disjssun 2932  preq12b 3154  unissintOLD 3242  uniintsn 3253  iinrab2 3319  intex 3465  intnex 3466  sucprc 3740  euuni 3807  rabsnt 3821  reuunisn 3822  onuninsuci 3921  dmxpid 4179  elreldm 4185  relimasn 4288  elimasni 4292  xpnz 4335  xpdisj1 4337  xpdisj2 4338  resdisj 4340  resdisjOLD 4341  dmxpss 4343  rnxpssOLD 4345  xpcan 4348  xpcan2 4350  dmsnopOLD 4368  unixp 4422  unixp0 4423  cnvresid 4488  funimacnv 4490  fconstOLD 4603  f1o00 4668  fvprc 4678  funfv 4731  funfv2f 4733  dffv2 4734  fvopabn 4749  fopabcos 4806  fconst5 4824  fnrnoprv 4966  1stval 5022  2ndval 5023  1st2val 5038  2nd2val 5039  1stconst 5070  curry2 5078  fsplit 5086  uniabio 5095  iotanul 5098  tz7.44-2 5137  dfrdg2 5141  rdgval 5148  om0 5201  oe0m 5202  oe0m0 5204  oe0 5206  oev2 5207  om0r 5221  oe1m 5226  oawordeulem 5236  oa00 5241  oarec 5244  oeworde 5268  oeoa 5272  oeoelem 5273  oeoe 5274  nnmsucrOLD 5296  oaabs 5309  nneob 5312  map0e 5401  en1 5485  fundmen 5487  mapsnen 5488  xpsnen 5494  xpcomen 5498  xpdom2 5501  sbthlem5 5514  sbthlem8 5517  fodomr 5547  mapdom2lem 5587  xpmapenlem2 5591  xpmapenlem4 5593  mapunen 5596  unifi 5648  fiint 5650  abfii3 5653  pwfi 5661  supsn 5681  ordtypelem1 5684  ordtypelem6 5689  inf3lema 5715  inf3lemd 5718  r1val1 5769  rankval2 5781  rankr1 5785  rankeq0 5807  rankxplim3 5825  scott0 5847  omsublim 5887  aceq5lem3 5899  kmlem2 5928  kmlem11 5937  numthlem 5945  zorn2lem1 5950  cardval 5975  cardaleph 6033  cardcf 6059  cfeq0 6062  cfom 6064  recmulpq 6222  genpv 6254  genpass 6264  addcompr 6275  mulcompr 6277  mulcmpblnrlem 6334  recexsrlem 6364  ssgt0sr 6369  addresr 6408  mulresr 6409  ax1id 6435  axcnre 6439  addcaniOLD 6506  negeui 6510  1re 6598  add20i 6782  msqge0i 6795  recextlem2 6875  mulcani 6878  mul0ori 6882  receui 6890  nn0addcl 7329  nn0mulcli 7331  znegcl 7372  elnn0nn 7380  zltp1le 7390  nneoi 7409  dfuzi 7414  uzindOLD 7420  nn0ind-raph 7426  ndmioo 7537  elioore 7554  seq1lem1 7722  seq1suclem 7729  seqz1 7790  exp0 7814  1exp 7827  mulexp 7836  exprec 7837  exprecOLD 7838  exple1 7852  sumsqne0i 7879  sq0i 7881  bernneq 7898  bernneqOLD 7899  discrlem3 7908  crne0i 7989  crreczi 7991  reim0b 8025  rereb 8026  abs00i 8093  abs1mi 8156  cau2i 8165  facp1 8188  faclbnd3 8199  faclbnd4lem1 8200  faclbnd4lem3 8202  faclbnd4lem4 8203  bcpasci 8221  dffsum 8258  csbfsumlem 8286  fsumrev 8289  fsumconst 8298  ser1ser0i 8308  binomlem1 8326  binomlem2 8327  binomlem3 8328  binomlem4 8329  binomlem6 8331  binomi 8332  climconsti 8354  caucvg3 8428  ser1clim0 8433  cvgcmp3cetlem1 8449  dfisum 8452  isumshfti 8465  isumshft2i 8466  georeclim 8502  geoisumr 8505  fsum0diag 8520  mulc1cncf 8541  ivthlem8 8550  dfef2i 8569  ef0lem 8572  efseq0ex 8573  efaddlem6 8605  efcan 8630  ef1tllem 8643  efgt0i 8669  sincossq 8726  cos2tsin 8729  absefi 8748  demoivre 8752  acdc3 8755  acdc2lem2 8758  acdc2 8759  acdc5lem2 8761  acdc5 8762  acdc 8764  xpnnen 8768  infxpidmlem4 8824  infxpidmlem8 8828  infxpidmlem10 8830  alephadd 8851  tgval2 8887  subtop 8916  indistop 8918  fctop 8920  cctop 8922  idcn 9042  cncnplem4 9054  metssba2 9087  metreslem 9099  metres 9100  metxptval 9107  blfval2 9113  cncfmet 9183  dscmet 9196  iscau 9214  xplm 9253  gid0 9338  grpsn 9340  grpidvallem 9341  grpidval 9342  gx0 9384  gxnn0neg 9386  gxnn0suc 9387  gaid 9454  ringsn 9490  vcoprne 9530  nvvcop 9545  bafval 9555  ipid 9702  iporthcom 9708  ip0r 9709  ip0l 9710  nmo0 9791  nmlno0lem 9793  nmlnoubi 9796  ipasslem2 9832  pythi 9851  siilem1 9852  siii 9854  ubthlem8 9879  minveclem19 9908  minveclem27 9916  sincosq1eq 10059  sinkpi 10063  coskpi 10064  sineq0re 10067  efifolem2 10077  efifolem7 10082  efif1lem5 10088  efper 10101  xp1st 10155  xp2nd 10156  upxp 10225  txcnopab 10228  subcld 10254  oefil2 10275  fsubbas 10281  filrn 10293  cncomp 10331  on1el3 10412  zrdivrng 10418  hvmul0 10525  hvsubid 10527  hvaddsubval 10534  hvsubeq0i 10562  hvsub0 10576  hi02 10596  orthcom 10607  bcseqi 10619  normgt0OLD 10626  normgt0 10627  normpythi 10642  hlim0 10738  hsn0elch 10753  ocsh 10789  occllem7 10812  omlsilem 10877  pjoc1i 10897  shjcom 10963  shs00i 11006  chj00i 11043  h1de2bi 11110  h1datomi 11137  fh1 11194  fh2 11195  cm2j 11196  nonbooli 11231  pjssge0ii 11262  hosubeq0i 11389  eigrei 11397  eigorthi 11400  kbpj 11517  0cnop 11540  0cnfn 11541  0lnfn 11546  nmop0 11547  nmfn0 11548  nmop0h 11553  nmlnop0iALT 11557  lnopco0i 11566  lnopeq0i 11569  nmcoplbi 11595  nmophmi 11598  lnopconi 11600  nmbdfnlbi 11615  nmcfnlbi 11624  lnfnconi 11627  nlelshi 11630  adjeq0 11661  nmopcoi 11665  unierri 11674  nmopleid 11710  opsqrlem1 11711  pjsdi2i 11729  pjclem1 11768  hstnmoc 11795  hst1h 11799  strlem3a 11824  strlem4 11826  golem1 11843  stcltrlem1 11848  mdsl1i 11893  mdslmd3i 11904  csmdsymi 11906  atoml2i 11955  atordi 11956  atabsi 11973  sumdmdlem2 11991  cdj3lem1 12006  bnj571 13289  bnj1416 13528  ghomsn 13631  cayleylem3 13643  divalglem8 13703  gcddvds 13722  gcdcl 13724  gcdeq0 13727  gcd0id 13729  gcdaddmlem 13734  eucalglt 13753  eucalg 13755  mulgcdlem2 13757  nepss 13820  epsetlike 13905  trcltr 13936  xporderlem 13948  frxp 13951  axfelem2 14032  axfelem8 14038  axfelem9 14039  moec 14351  neiopne 14354  fldsqcp2 14378  eloi 14400  rnxpid 14409  repfuntw 14502  unprj 14511  nfwpr4c 14630  prodeq123i 14664  mgmrddd 14727  cmprtr2 14761  imtr 14762  rnplrnml3 14768  eqindhome 14895  clindistop 14962  topsinind 14967  singcon 14968  invtrgrp 14979  miminf 15028  ismona 15158  elfiun 15369  fictb 15371  finsschain 15373  ordtypelem1OLD 15375  ordtypelem6OLD 15380  omsublimOLD 15396  topbnd 15408  cnsubsp2 15427  compsublem 15430  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem2 15438  connsub 15443  cnconn 15444  reconnlem1 15446  ivthALT 15454  2ndcctbss 15478  comppfsc 15517  ufileu 15573  filufint 15574  filcon 15580  flimcls 15588  flimfnfcls 15615  filnetlem5 15644  filnet 15645  sdc 15811  fdc 15812  mettrifi2 15848  oprpiece1res2 15881  txsubsp 15912  txcld 15914  cnoprab1 15921  cnoprab2 15922  txmet 15925  bndss 15942  blbnd 15943  totbndbnd 15944  heiborlem8 15962  heiborlem9 15963  heiborlem11 15965  heiborlem13 15967  heiborlem32 15986  bfplem11 16008  rrndm 16015  ismrer1 16024  exidreslem 16030  isablda 16035  phtpycom 16050  phtpycolem2 16052  reparpht 16065  pcoval2 16075  pco0 16077  pco1 16078  pcohtpylem2 16081  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1gp 16095  divrngcl 16110  ispridlc 16218  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  cmtval 16938  cvrval 16988  glbconx 17029  grpinvfvalNEW 17125  pmapglb2 17253  pmapglb2x 17254  padd01 17272  padd02 17273  pmod2i 17310  pmod 17311  pmodl42 17312  polval2 17319  pol0 17322  osumcllem3 17366

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain