Theorem eqtrdi 2219

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

Hypotheses

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

Assertion

Ref	Expression
eqtrdi	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtrdi

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  eqtr2di  2220  eqtr4di  2221  3eqtr3g  2226  3eqtr4a  2229  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  csbprc  3460  un00  3461  disjssun  3478  disjpr2  3647  tppreq3  3686  diftpsn3  3721  preq12b  3757  intsng  3865  uniintsnr  3867  rint0  3870  riin0  3944  iununir  3956  intexr  4136  sucprc  4397  op1stbg  4464  elreldm  4837  xpeq0r  5033  xpdisj1  5035  xpdisj2  5036  resdisj  5039  xpima1  5057  xpima2m  5058  elxp4  5098  unixp0im  5147  uniabio  5170  iotass  5177  cnvresid  5272  funimacnv  5274  f1o00  5477  dffv4g  5493  fnrnfv  5543  feqresmpt  5550  dffn5imf  5551  funfvdm2f  5561  fvun1  5562  fvmpt2  5579  fndmin  5603  fmptcof  5663  fmptcos  5664  fvunsng  5690  fvpr1  5700  fnrnov  5998  offval  6068  ofrfval  6069  op1std  6127  op2ndd  6128  fmpoco  6195  tpostpos  6243  tfr0  6302  rdgival  6361  frec0g  6376  2oconcl  6418  om0  6437  oei0  6438  oasuc  6443  omv2  6444  nnm0r  6458  uniqs2  6573  en1  6777  en1bg  6778  fundmen  6784  mapsnen  6789  xpsnen  6799  xpcomco  6804  xpdom2  6809  xpmapenlem  6827  exmidpweq  6887  unsnfidcex  6897  fiintim  6906  ssfirab  6911  sbthlemi8  6941  elfi2  6949  fi0  6952  fieq0  6953  djudom  7070  ismkvnex  7131  nninfwlpoimlemg  7151  en2other2  7173  exmidfodomrlemim  7178  nq0m0r  7418  addpinq1  7426  genipv  7471  genpelvl  7474  genpelvu  7475  cauappcvgprlem1  7621  caucvgsrlemoffres  7762  addresr  7799  mulresr  7800  axcnre  7843  add20  8393  rimul  8504  rereim  8505  mulreim  8523  sup3exmid  8873  fv0p1e1  8993  div4p1lem1div2  9131  nnm1nn0  9176  znegcl  9243  peano2z  9248  nneoor  9314  nn0ind-raph  9329  xnegneg  9790  xltnegi  9792  xaddpnf1  9803  xnegid  9816  xnn0xadd0  9824  xnegdi  9825  xsubge0  9838  xposdif  9839  xlesubadd  9840  xleaddadd  9844  fz0to4untppr  10080  fzo0to2pr  10174  fldiv4p1lem1div2  10261  mulp1mod1  10321  frecfzennn  10382  iseqf1olemqk  10450  exp0  10480  expp1  10483  expnegap0  10484  1exp  10505  mulexp  10515  m1expeven  10523  sq0i  10567  bernneq  10596  facp1  10664  faclbnd3  10677  facubnd  10679  bcval5  10697  hashinfom  10712  hashsng  10733  hashxp  10761  resunimafz0  10766  zfz1iso  10776  imre  10815  reim0b  10826  rereb  10827  resqrexlemover  10974  resqrexlemcalc1  10978  abs00bd  11030  maxabslemlub  11171  xrmaxiflemcom  11212  xrmaxadd  11224  climconst  11253  isumz  11352  fsumf1o  11353  fsumcllem  11362  fsumadd  11369  fsumxp  11399  fsumcnv  11400  fsummulc2  11411  fsumconst  11417  fsumabs  11428  telfsumo  11429  fsumparts  11433  fsumrelem  11434  fsumiun  11440  binomlem  11446  binom  11447  binom11  11449  isumsplit  11454  arisum  11461  arisum2  11462  trireciplem  11463  georeclim  11476  cvgratnnlemseq  11489  prodfrecap  11509  prod1dc  11549  fprodf1o  11551  fprodcl2lem  11568  fprodcllem  11569  fprodfac  11578  fprod2d  11586  fprodxp  11587  fprodcnv  11588  fprodrec  11592  fprodmodd  11604  ef0lem  11623  ege2le3  11634  efaddlem  11637  efcan  11639  eft0val  11656  ef4p  11657  efgt1p2  11658  efi4p  11680  sincossq  11711  cos2tsin  11714  absefi  11731  demoivreALT  11736  p1modz1  11756  dvdsabseq  11807  odd2np1lem  11831  oddp1even  11835  opoe  11854  m1expo  11859  m1exp1  11860  nn0o1gt2  11864  nninfdcex  11908  gcddvds  11918  gcdcl  11921  gcdeq0  11932  gcd0id  11934  bezoutr1  11988  nnmindc  11989  nnminle  11990  eucalg  12013  lcm0val  12019  lcmid  12034  rpmul  12052  dfphi2  12174  phiprmpw  12176  hashgcdeq  12193  odzdvds  12199  nnnn0modprm0  12209  pythagtriplem4  12222  pythagtriplem12  12229  pcaddlem  12292  pcmpt  12295  pockthi  12310  ennnfonelem0  12360  ennnfonelem1  12362  ennnfonelemhdmp1  12364  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemf1  12373  ctiunctlemfo  12394  setsresg  12454  strle1g  12508  restid2  12588  tgval2  12845  tgidm  12868  epttop  12884  tgrest  12963  restco  12968  restsn  12974  tgcn  13002  cnptopresti  13032  cnptoprest  13033  txbas  13052  upxp  13066  txrest  13070  txdis  13071  txhmeo  13113  txswaphmeolem  13114  xblss2ps  13198  xblss2  13199  qtopbasss  13315  fsumcncntop  13350  limcimolemlt  13427  dvcnp2cntop  13457  dvcoapbr  13465  dvexp  13469  dvexp2  13470  dveflem  13481  dvef  13482  sin0pilem1  13496  sin2kpi  13526  cos2kpi  13527  coseq0q4123  13549  coseq0negpitopi  13551  sincosq1eq  13554  sinkpi  13562  coskpi  13563  1cxp  13615  lgslem2  13696  lgsfcl2  13701  lgs0  13708  lgs2  13712  lgsneg  13719  lgsdilem  13722  lgsdir2lem4  13726  lgsdir2lem5  13727  lgsne0  13733  lgssq  13735  lgssq2  13736  2sqlem9  13754  2sqlem10  13755  ex-ceil  13761  bj-intexr  13943  exmid1stab  14033  peano3nninf  14040  nninfall  14042  isomninnlem  14062  iswomni0  14083  ismkvnnlem  14084  nconstwlpolem0  14094