Theorem eqtrdi 2253

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 2237	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197

This theorem is referenced by:  eqtr2di  2254  eqtr4di  2255  3eqtr3g  2260  3eqtr4a  2263  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  csbprc  3505  un00  3506  disjssun  3523  disjpr2  3696  tppreq3  3735  diftpsn3  3773  preq12b  3810  intsng  3918  uniintsnr  3920  rint0  3923  riin0  3998  iununir  4010  intexr  4193  exmid1stab  4251  sucprc  4458  op1stbg  4525  elreldm  4903  xpeq0r  5104  xpdisj1  5106  xpdisj2  5107  resdisj  5110  xpima1  5128  xpima2m  5129  elxp4  5169  unixp0im  5218  uniabio  5241  iotass  5248  cnvresid  5347  funimacnv  5349  fimadmfo  5506  f1o00  5556  dffv4g  5572  fv2prc  5612  fnrnfv  5624  feqresmpt  5632  dffn5imf  5633  funfvdm2f  5643  fvun1  5644  fvmpt2  5662  fndmin  5686  fmptcof  5746  fmptcos  5747  funopdmsn  5763  fvunsng  5777  fvpr1  5787  fnrnov  6091  offval  6165  ofrfval  6166  op1std  6233  op2ndd  6234  fmpoco  6301  tpostpos  6349  tfr0  6408  rdgival  6467  frec0g  6482  2oconcl  6524  om0  6543  oei0  6544  oasuc  6549  omv2  6550  nnm0r  6564  uniqs2  6681  en1  6890  en1bg  6891  fundmen  6897  mapsnen  6902  en2  6911  xpsnen  6915  xpcomco  6920  xpdom2  6925  xpmapenlem  6945  exmidpweq  7005  unsnfidcex  7016  fiintim  7027  ssfirab  7032  sbthlemi8  7065  elfi2  7073  fi0  7076  fieq0  7077  djudom  7194  ismkvnex  7256  nninfwlpoimlemg  7276  en2other2  7303  exmidfodomrlemim  7308  nq0m0r  7568  addpinq1  7576  genipv  7621  genpelvl  7624  genpelvu  7625  cauappcvgprlem1  7771  caucvgsrlemoffres  7912  addresr  7949  mulresr  7950  axcnre  7993  add20  8546  rimul  8657  rereim  8658  mulreim  8676  sup3exmid  9029  fv0p1e1  9150  div4p1lem1div2  9290  nnm1nn0  9335  znegcl  9402  peano2z  9407  nneoor  9474  nn0ind-raph  9489  xnegneg  9954  xltnegi  9956  xaddpnf1  9967  xnegid  9980  xnn0xadd0  9988  xnegdi  9989  xsubge0  10002  xposdif  10003  xlesubadd  10004  xleaddadd  10008  fz0to4untppr  10245  fzo0to2pr  10345  nninfdcex  10378  fldiv4p1lem1div2  10446  fldiv4lem1div2  10448  mulp1mod1  10508  frecfzennn  10569  iseqf1olemqk  10650  exp0  10686  expp1  10689  expnegap0  10690  1exp  10711  mulexp  10721  m1expeven  10729  sq0i  10774  bernneq  10803  facp1  10873  faclbnd3  10886  facubnd  10888  bcval5  10906  hashinfom  10921  hashsng  10941  hashxp  10969  resunimafz0  10974  zfz1iso  10984  hash2en  10986  lsw1  11041  imre  11104  reim0b  11115  rereb  11116  resqrexlemover  11263  resqrexlemcalc1  11267  abs00bd  11319  maxabslemlub  11460  xrmaxiflemcom  11502  xrmaxadd  11514  climconst  11543  isumz  11642  fsumf1o  11643  fsumcllem  11652  fsumadd  11659  fsumxp  11689  fsumcnv  11690  fsummulc2  11701  fsumconst  11707  fsumabs  11718  telfsumo  11719  fsumparts  11723  fsumrelem  11724  fsumiun  11730  binomlem  11736  binom  11737  binom11  11739  isumsplit  11744  arisum  11751  arisum2  11752  trireciplem  11753  georeclim  11766  cvgratnnlemseq  11779  prodfrecap  11799  prod1dc  11839  fprodf1o  11841  fprodcl2lem  11858  fprodcllem  11859  fprodfac  11868  fprod2d  11876  fprodxp  11877  fprodcnv  11878  fprodrec  11882  fprodmodd  11894  ef0lem  11913  ege2le3  11924  efaddlem  11927  efcan  11929  eft0val  11946  ef4p  11947  efgt1p2  11948  efi4p  11970  sincossq  12001  cos2tsin  12004  absefi  12022  demoivreALT  12027  p1modz1  12047  dvdsabseq  12100  odd2np1lem  12125  oddp1even  12129  opoe  12148  m1expo  12153  m1exp1  12154  nn0o1gt2  12158  bitsinv1  12215  gcddvds  12226  gcdcl  12229  gcdeq0  12240  gcd0id  12242  bezoutr1  12296  nnmindc  12297  nnminle  12298  eucalg  12323  lcm0val  12329  lcmid  12344  rpmul  12362  dfphi2  12484  phiprmpw  12486  hashgcdeq  12504  odzdvds  12510  nnnn0modprm0  12520  pythagtriplem4  12533  pythagtriplem12  12540  pcaddlem  12604  pcmpt  12608  pockthi  12623  4sqlem12  12667  2expltfac  12704  ennnfonelem0  12718  ennnfonelem1  12720  ennnfonelemhdmp1  12722  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemf1  12731  ctiunctlemfo  12752  setsresg  12812  strressid  12845  strle1g  12880  restid2  13022  prdsbas3  13061  gsumwmhm  13272  grplactcnv  13376  mulg0  13403  mulgnn0gsum  13406  mulgneg  13418  mulgneg2  13434  gsumfzconst  13619  gsumfzsnfd  13623  gsumfzfsumlem0  14290  zrhval2  14323  mpl0fi  14406  tgval2  14465  tgidm  14488  epttop  14504  tgrest  14583  restco  14588  restsn  14594  tgcn  14622  cnptopresti  14652  cnptoprest  14653  txbas  14672  upxp  14686  txrest  14690  txdis  14691  txhmeo  14733  txswaphmeolem  14734  xblss2ps  14818  xblss2  14819  qtopbasss  14935  fsumcncntop  14981  hoverb  15062  limcimolemlt  15078  dvcnp2cntop  15113  dvcoapbr  15121  dvexp  15125  dvexp2  15126  dvmptid  15130  dveflem  15140  dvef  15141  plymullem1  15162  plyadd  15165  plymul  15166  plycoeid3  15171  plycjlemc  15174  plycj  15175  sin0pilem1  15195  sin2kpi  15225  cos2kpi  15226  coseq0q4123  15248  coseq0negpitopi  15250  sincosq1eq  15253  sinkpi  15261  coskpi  15262  1cxp  15314  mpodvdsmulf1o  15404  lgslem2  15420  lgsfcl2  15425  lgs0  15432  lgs2  15436  lgsneg  15443  lgsdilem  15446  lgsdir2lem4  15450  lgsdir2lem5  15451  lgsne0  15457  lgssq  15459  lgssq2  15460  gausslemma2dlem3  15482  gausslemma2dlem4  15483  lgseisenlem1  15489  lgsquadlem2  15497  lgsquad2lem2  15501  lgsquad3  15503  m1lgs  15504  2lgslem1a2  15506  2lgsoddprmlem3  15530  2sqlem9  15543  2sqlem10  15544  ex-ceil  15595  bj-intexr  15777  peano3nninf  15877  nninfall  15879  isomninnlem  15902  iswomni0  15923  ismkvnnlem  15924  nconstwlpolem0  15935