Theorem syl6eq 2188

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

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 9	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2172	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  syl6req  2189  syl6eqr  2190  3eqtr3g  2195  3eqtr4a  2198  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  csbprc  3408  un00  3409  disjssun  3426  disjpr2  3587  tppreq3  3626  diftpsn3  3661  preq12b  3697  intsng  3805  uniintsnr  3807  rint0  3810  riin0  3884  iununir  3896  intexr  4075  sucprc  4334  op1stbg  4400  elreldm  4765  xpeq0r  4961  xpdisj1  4963  xpdisj2  4964  resdisj  4967  xpima1  4985  xpima2m  4986  elxp4  5026  unixp0im  5075  uniabio  5098  iotass  5105  cnvresid  5197  funimacnv  5199  f1o00  5402  dffv4g  5418  fnrnfv  5468  feqresmpt  5475  dffn5imf  5476  funfvdm2f  5486  fvun1  5487  fvmpt2  5504  fndmin  5527  fmptcof  5587  fmptcos  5588  fvunsng  5614  fvpr1  5624  fnrnov  5916  offval  5989  ofrfval  5990  op1std  6046  op2ndd  6047  fmpoco  6113  tpostpos  6161  tfr0  6220  rdgival  6279  frec0g  6294  2oconcl  6336  om0  6354  oei0  6355  oasuc  6360  omv2  6361  nnm0r  6375  uniqs2  6489  en1  6693  en1bg  6694  fundmen  6700  mapsnen  6705  xpsnen  6715  xpcomco  6720  xpdom2  6725  xpmapenlem  6743  unsnfidcex  6808  fiintim  6817  ssfirab  6822  sbthlemi8  6852  elfi2  6860  fi0  6863  fieq0  6864  djudom  6978  ismkvnex  7029  en2other2  7052  exmidfodomrlemim  7057  nq0m0r  7264  addpinq1  7272  genipv  7317  genpelvl  7320  genpelvu  7321  cauappcvgprlem1  7467  caucvgsrlemoffres  7608  addresr  7645  mulresr  7646  axcnre  7689  add20  8236  rimul  8347  rereim  8348  mulreim  8366  sup3exmid  8715  fv0p1e1  8835  div4p1lem1div2  8973  nnm1nn0  9018  znegcl  9085  peano2z  9090  nneoor  9153  nn0ind-raph  9168  xnegneg  9616  xltnegi  9618  xaddpnf1  9629  xnegid  9642  xnn0xadd0  9650  xnegdi  9651  xsubge0  9664  xposdif  9665  xlesubadd  9666  xleaddadd  9670  fzo0to2pr  9995  fldiv4p1lem1div2  10078  mulp1mod1  10138  frecfzennn  10199  iseqf1olemqk  10267  exp0  10297  expp1  10300  expnegap0  10301  1exp  10322  mulexp  10332  m1expeven  10340  sq0i  10384  bernneq  10412  facp1  10476  faclbnd3  10489  facubnd  10491  bcval5  10509  hashinfom  10524  hashsng  10544  hashxp  10572  resunimafz0  10574  zfz1iso  10584  imre  10623  reim0b  10634  rereb  10635  resqrexlemover  10782  resqrexlemcalc1  10786  abs00bd  10838  maxabslemlub  10979  xrmaxiflemcom  11018  xrmaxadd  11030  climconst  11059  isumz  11158  fsumf1o  11159  fsumcllem  11168  fsumadd  11175  fsumxp  11205  fsumcnv  11206  fsummulc2  11217  fsumconst  11223  fsumabs  11234  telfsumo  11235  fsumparts  11239  fsumrelem  11240  fsumiun  11246  binomlem  11252  binom  11253  binom11  11255  isumsplit  11260  arisum  11267  arisum2  11268  trireciplem  11269  georeclim  11282  cvgratnnlemseq  11295  prodfrecap  11315  ef0lem  11366  ege2le3  11377  efaddlem  11380  efcan  11382  eft0val  11399  ef4p  11400  efgt1p2  11401  efi4p  11424  sincossq  11455  cos2tsin  11458  absefi  11475  demoivreALT  11480  dvdsabseq  11545  odd2np1lem  11569  oddp1even  11573  opoe  11592  m1expo  11597  m1exp1  11598  nn0o1gt2  11602  gcddvds  11652  gcdcl  11655  gcdeq0  11665  gcd0id  11667  bezoutr1  11721  eucalg  11740  lcm0val  11746  lcmid  11761  rpmul  11779  dfphi2  11896  phiprmpw  11898  hashgcdeq  11904  ennnfonelem0  11918  ennnfonelem1  11920  ennnfonelemhdmp1  11922  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemf1  11931  ctiunctlemfo  11952  setsresg  11997  strle1g  12049  restid2  12129  tgval2  12220  tgidm  12243  epttop  12259  tgrest  12338  restco  12343  restsn  12349  tgcn  12377  cnptopresti  12407  cnptoprest  12408  txbas  12427  upxp  12441  txrest  12445  txdis  12446  txhmeo  12488  txswaphmeolem  12489  xblss2ps  12573  xblss2  12574  qtopbasss  12690  fsumcncntop  12725  limcimolemlt  12802  dvcnp2cntop  12832  dvcoapbr  12840  dvexp  12844  dvexp2  12845  dveflem  12855  dvef  12856  sin0pilem1  12862  sin2kpi  12892  cos2kpi  12893  coseq0q4123  12915  coseq0negpitopi  12917  sincosq1eq  12920  sinkpi  12928  coskpi  12929  ex-ceil  12938  bj-intexr  13106  exmid1stab  13195  peano3nninf  13201  nninfall  13204  isomninnlem  13225