Theorem syl5eq 2211

Description: Renamed to eqtrid 2210. Kept during a transition period. DO NOT USE. (Contributed by NM, 21-Jun-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl5eq	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl5eq

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqtr2id  2212  eqtr3id  2213  3eqtr3a  2223  3eqtr4g  2224  csbtt  3057  csbvarg  3073  csbie2g  3095  rabbi2dva  3330  csbprc  3454  disjssun  3472  disjpr2  3640  prprc2  3685  difprsn2  3713  opprc  3779  intsng  3858  riinm  3938  iinxsng  3939  iunxprg  3946  rintm  3958  sucprc  4390  unisucg  4392  xpriindim  4742  relop  4754  dmxpm  4824  riinint  4865  resabs1  4913  resabs2  4915  resima2  4918  xpssres  4919  resopab2  4931  imasng  4969  ndmima  4981  xpdisj1  5028  xpdisj2  5029  djudisj  5031  resdisj  5032  rnxpm  5033  xpima1  5050  xpima2m  5051  dmsnsnsng  5081  rnsnopg  5082  rnpropg  5083  mptiniseg  5098  dfco2a  5104  relcoi1  5135  unixpm  5139  iotaval  5164  funtp  5241  fnun  5294  fnresdisj  5298  fnima  5306  fnimaeq0  5309  fcoi1  5368  f1orescnv  5448  foun  5451  resdif  5454  tz6.12-2  5477  fveu  5478  tz6.12-1  5513  fvun2  5553  fvopab3ig  5560  f1oresrab  5650  dfmptg  5664  ressnop0  5666  fvunsng  5679  fnsnsplitss  5684  fsnunfv  5686  fvpr1  5689  fvpr2  5690  fvpr1g  5691  fvpr2g  5692  fvtp1g  5693  fvtp2g  5694  fvtp3g  5695  fvtp2  5697  fvtp3  5698  f1oiso2  5795  riotaund  5832  ovprc  5877  resoprab2  5939  fnoprabg  5943  ovidig  5959  ovigg  5962  ov6g  5979  ovconst2  5993  offval2  6065  ot1stg  6120  ot2ndg  6121  ot3rdgg  6122  fmpoco  6184  algrflemg  6198  tpostpos2  6233  rdgisuc1  6352  frec0g  6365  frecsuclem  6374  frecrdg  6376  oasuc  6432  oa1suc  6435  omsuc  6440  nnm1  6492  nnm2  6493  dfec2  6504  errn  6523  ixpsnval  6667  ixpintm  6691  mapen  6812  xpmapenlem  6815  phplem2  6819  undifdc  6889  fisseneq  6897  ssfirab  6899  eqinfti  6985  infvalti  6987  infsnti  6995  casef  7053  caseinl  7056  caseinr  7057  djudom  7058  ctssdccl  7076  exmidfodomrlemim  7157  1qec  7329  mulidnq  7330  addpinq1  7405  suplocexprlem2b  7655  suplocexprlemlub  7665  0idsr  7708  1idsr  7709  caucvgsrlemoffres  7741  caucvgsr  7743  mulresr  7779  pitonnlem2  7788  ax1rid  7818  axcnre  7822  negid  8145  subneg  8147  negneg  8148  dfinfre  8851  2times  8985  infrenegsupex  9532  rexneg  9766  xaddpnf2  9783  xaddmnf1  9784  xaddmnf2  9785  fseq1p1m1  10029  fzosplitprm1  10169  intfracq  10255  frec2uz0d  10334  frec2uzrdg  10344  frecuzrdg0  10348  frecuzrdgg  10351  frecuzrdg0t  10357  seq3val  10393  seqvalcd  10394  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  iseqf1olemfvp  10432  seq3f1olemqsum  10435  sqval  10513  iexpcyc  10559  binom3  10572  faclbnd  10654  faclbnd2  10655  bcn1  10671  hashinfom  10691  hashennn  10693  hashxp  10739  shftlem  10758  shftuz  10759  shftidt  10775  reim0  10803  remullem  10813  resqrexlemf1  10950  resqrexlemcalc3  10958  absexpzap  11022  absimle  11026  amgm2  11060  minmax  11171  mingeb  11183  2zinfmin  11184  xrmaxiflemval  11191  xrmaxadd  11202  infxrnegsupex  11204  xrminmax  11206  summodc  11324  fsum3  11328  sumsnf  11350  sumsns  11356  isumclim3  11364  isumge0  11371  fsump1i  11374  fsum2dlemstep  11375  fisumcom2  11379  fsumshftm  11386  fsumconst  11395  fsumiun  11418  hashrabrex  11422  hashuni  11423  binom11  11427  isumsplit  11432  geo2sum  11455  mertensabs  11478  prodmodc  11519  fprodseq  11524  prodsnf  11533  prodsns  11544  fprodconst  11561  fprod2dlemstep  11563  fprodcom2fi  11567  efgt1p2  11636  efgt1p  11637  resinval  11656  recosval  11657  cosadd  11678  ef01bndlem  11697  eirraplem  11717  ialgr0  11976  algrp1  11978  eucalg  11991  phiprmpw  12154  phiprm  12155  prmdiv  12167  pythagtriplem12  12207  pythagtriplem14  12209  pythagtriplem16  12211  pceu  12227  pcfac  12280  prmpwdvds  12285  4sqlem5  12312  mul4sqlem  12323  ennnfonelem0  12338  ennnfonelemfun  12350  ennnfonelemf1  12351  ennnfonelemrn  12352  ctinfomlemom  12360  nninfdclemp1  12383  ndxid  12418  setsfun0  12430  setsresg  12432  setscom  12434  strslfv2d  12436  ressid2  12454  ressval2  12455  plusffvalg  12593  tgidm  12714  tgrest  12809  ssidcn  12850  txcnmpt  12913  txcn  12915  blres  13074  mopnval  13082  remetdval  13179  divccncfap  13217  cncfmet  13219  cncfcncntop  13220  cnplimcim  13276  cnplimclemr  13278  limccnpcntop  13284  limccnp2cntop  13286  dvexp  13315  sin0pilem1  13342  pilem3  13344  ef2kpi  13367  sin2pim  13374  cos2pim  13375  sinmpi  13376  cosmpi  13377  sinppi  13378  cosppi  13379  sinhalfpip  13381  sinhalfpim  13382  coshalfpip  13383  coshalfpim  13384  tangtx  13399  1cxp  13461  ecxp  13462  rplogb1  13506  rpelogb  13507  binom4  13537  lgslem1  13541  2sqlem8  13599  ex-ceil  13607  qdencn  13906  cvgcmp2nlemabs  13911  trilpolemlt1  13920  nconstwlpolem0  13941