Theorem syl6eq 2163

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

Hypotheses

Ref	Expression
syl6eq.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eq.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6eq	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl6eq

Step	Hyp	Ref	Expression
1		syl6eq.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eq.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2147	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

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

This theorem is referenced by:  syl6req  2164  syl6eqr  2165  3eqtr3g  2170  3eqtr4a  2173  cbvralcsf  3028  cbvrexcsf  3029  cbvreucsf  3030  cbvrabcsf  3031  csbprc  3374  un00  3375  disjssun  3392  disjpr2  3553  tppreq3  3592  diftpsn3  3627  preq12b  3663  intsng  3771  uniintsnr  3773  rint0  3776  riin0  3850  iununir  3862  intexr  4035  sucprc  4294  op1stbg  4360  elreldm  4725  xpeq0r  4919  xpdisj1  4921  xpdisj2  4922  resdisj  4925  xpima1  4943  xpima2m  4944  elxp4  4984  unixp0im  5033  uniabio  5056  iotass  5063  cnvresid  5155  funimacnv  5157  f1o00  5358  dffv4g  5372  fnrnfv  5422  feqresmpt  5429  dffn5imf  5430  funfvdm2f  5440  fvun1  5441  fvmpt2  5458  fndmin  5481  fmptcof  5541  fmptcos  5542  fvunsng  5568  fvpr1  5578  fnrnov  5870  offval  5943  ofrfval  5944  op1std  6000  op2ndd  6001  fmpoco  6067  tpostpos  6115  tfr0  6174  rdgival  6233  frec0g  6248  2oconcl  6290  om0  6308  oei0  6309  oasuc  6314  omv2  6315  nnm0r  6329  uniqs2  6443  en1  6647  en1bg  6648  fundmen  6654  mapsnen  6659  xpsnen  6668  xpcomco  6673  xpdom2  6678  xpmapenlem  6696  unsnfidcex  6761  fiintim  6770  ssfirab  6774  sbthlemi8  6804  elfi2  6812  fi0  6815  fieq0  6816  djudom  6930  ismkvnex  6979  en2other2  7000  exmidfodomrlemim  7005  nq0m0r  7212  addpinq1  7220  genipv  7265  genpelvl  7268  genpelvu  7269  cauappcvgprlem1  7415  caucvgsrlemoffres  7542  addresr  7572  mulresr  7573  axcnre  7616  add20  8155  rimul  8265  rereim  8266  mulreim  8284  sup3exmid  8625  fv0p1e1  8745  div4p1lem1div2  8877  nnm1nn0  8922  znegcl  8989  peano2z  8994  nneoor  9057  nn0ind-raph  9072  xnegneg  9509  xltnegi  9511  xaddpnf1  9522  xnegid  9535  xnn0xadd0  9543  xnegdi  9544  xsubge0  9557  xposdif  9558  xlesubadd  9559  xleaddadd  9563  fzo0to2pr  9888  fldiv4p1lem1div2  9971  mulp1mod1  10031  frecfzennn  10092  iseqf1olemqk  10160  exp0  10190  expp1  10193  expnegap0  10194  1exp  10215  mulexp  10225  m1expeven  10233  sq0i  10277  bernneq  10305  facp1  10369  faclbnd3  10382  facubnd  10384  bcval5  10402  hashinfom  10417  hashsng  10437  hashxp  10465  resunimafz0  10467  zfz1iso  10477  imre  10516  reim0b  10527  rereb  10528  resqrexlemover  10674  resqrexlemcalc1  10678  abs00bd  10730  maxabslemlub  10871  xrmaxiflemcom  10910  xrmaxadd  10922  climconst  10951  isumz  11050  fsumf1o  11051  fsumcllem  11060  fsumadd  11067  fsumxp  11097  fsumcnv  11098  fsummulc2  11109  fsumconst  11115  fsumabs  11126  telfsumo  11127  fsumparts  11131  fsumrelem  11132  fsumiun  11138  binomlem  11144  binom  11145  binom11  11147  isumsplit  11152  arisum  11159  arisum2  11160  trireciplem  11161  georeclim  11174  cvgratnnlemseq  11187  ef0lem  11217  ege2le3  11228  efaddlem  11231  efcan  11233  eft0val  11250  ef4p  11251  efgt1p2  11252  efi4p  11275  sincossq  11306  cos2tsin  11309  absefi  11325  demoivreALT  11330  dvdsabseq  11393  odd2np1lem  11417  oddp1even  11421  opoe  11440  m1expo  11445  m1exp1  11446  nn0o1gt2  11450  gcddvds  11500  gcdcl  11503  gcdeq0  11513  gcd0id  11515  bezoutr1  11567  eucalg  11586  lcm0val  11592  lcmid  11607  rpmul  11625  dfphi2  11741  phiprmpw  11743  hashgcdeq  11749  ennnfonelem0  11763  ennnfonelem1  11765  ennnfonelemhdmp1  11767  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ennnfonelemf1  11776  ctiunctlemfo  11795  setsresg  11840  strle1g  11892  restid2  11972  tgval2  12063  tgidm  12086  epttop  12102  tgrest  12181  restco  12186  restsn  12192  tgcn  12219  cnptopresti  12249  cnptoprest  12250  txbas  12269  upxp  12283  txrest  12287  txdis  12288  xblss2ps  12393  xblss2  12394  qtopbasss  12510  fsumcncntop  12542  limcimolemlt  12589  dvcnp2cntop  12618  ex-ceil  12631  bj-intexr  12798  exmid1stab  12887  peano3nninf  12893  nninfall  12896  isomninnlem  12917