Theorem eqtrdi 2242

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtr2di  2243  eqtr4di  2244  3eqtr3g  2249  3eqtr4a  2252  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  csbprc  3493  un00  3494  disjssun  3511  disjpr2  3683  tppreq3  3722  diftpsn3  3760  preq12b  3797  intsng  3905  uniintsnr  3907  rint0  3910  riin0  3985  iununir  3997  intexr  4180  exmid1stab  4238  sucprc  4444  op1stbg  4511  elreldm  4889  xpeq0r  5089  xpdisj1  5091  xpdisj2  5092  resdisj  5095  xpima1  5113  xpima2m  5114  elxp4  5154  unixp0im  5203  uniabio  5226  iotass  5233  cnvresid  5329  funimacnv  5331  fimadmfo  5486  f1o00  5536  dffv4g  5552  fv2prc  5592  fnrnfv  5604  feqresmpt  5612  dffn5imf  5613  funfvdm2f  5623  fvun1  5624  fvmpt2  5642  fndmin  5666  fmptcof  5726  fmptcos  5727  fvunsng  5753  fvpr1  5763  fnrnov  6066  offval  6140  ofrfval  6141  op1std  6203  op2ndd  6204  fmpoco  6271  tpostpos  6319  tfr0  6378  rdgival  6437  frec0g  6452  2oconcl  6494  om0  6513  oei0  6514  oasuc  6519  omv2  6520  nnm0r  6534  uniqs2  6651  en1  6855  en1bg  6856  fundmen  6862  mapsnen  6867  xpsnen  6877  xpcomco  6882  xpdom2  6887  xpmapenlem  6907  exmidpweq  6967  unsnfidcex  6978  fiintim  6987  ssfirab  6992  sbthlemi8  7025  elfi2  7033  fi0  7036  fieq0  7037  djudom  7154  ismkvnex  7216  nninfwlpoimlemg  7236  en2other2  7258  exmidfodomrlemim  7263  nq0m0r  7518  addpinq1  7526  genipv  7571  genpelvl  7574  genpelvu  7575  cauappcvgprlem1  7721  caucvgsrlemoffres  7862  addresr  7899  mulresr  7900  axcnre  7943  add20  8495  rimul  8606  rereim  8607  mulreim  8625  sup3exmid  8978  fv0p1e1  9099  div4p1lem1div2  9239  nnm1nn0  9284  znegcl  9351  peano2z  9356  nneoor  9422  nn0ind-raph  9437  xnegneg  9902  xltnegi  9904  xaddpnf1  9915  xnegid  9928  xnn0xadd0  9936  xnegdi  9937  xsubge0  9950  xposdif  9951  xlesubadd  9952  xleaddadd  9956  fz0to4untppr  10193  fzo0to2pr  10288  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  mulp1mod1  10439  frecfzennn  10500  iseqf1olemqk  10581  exp0  10617  expp1  10620  expnegap0  10621  1exp  10642  mulexp  10652  m1expeven  10660  sq0i  10705  bernneq  10734  facp1  10804  faclbnd3  10817  facubnd  10819  bcval5  10837  hashinfom  10852  hashsng  10872  hashxp  10900  resunimafz0  10905  zfz1iso  10915  imre  10998  reim0b  11009  rereb  11010  resqrexlemover  11157  resqrexlemcalc1  11161  abs00bd  11213  maxabslemlub  11354  xrmaxiflemcom  11395  xrmaxadd  11407  climconst  11436  isumz  11535  fsumf1o  11536  fsumcllem  11545  fsumadd  11552  fsumxp  11582  fsumcnv  11583  fsummulc2  11594  fsumconst  11600  fsumabs  11611  telfsumo  11612  fsumparts  11616  fsumrelem  11617  fsumiun  11623  binomlem  11629  binom  11630  binom11  11632  isumsplit  11637  arisum  11644  arisum2  11645  trireciplem  11646  georeclim  11659  cvgratnnlemseq  11672  prodfrecap  11692  prod1dc  11732  fprodf1o  11734  fprodcl2lem  11751  fprodcllem  11752  fprodfac  11761  fprod2d  11769  fprodxp  11770  fprodcnv  11771  fprodrec  11775  fprodmodd  11787  ef0lem  11806  ege2le3  11817  efaddlem  11820  efcan  11822  eft0val  11839  ef4p  11840  efgt1p2  11841  efi4p  11863  sincossq  11894  cos2tsin  11897  absefi  11915  demoivreALT  11920  p1modz1  11940  dvdsabseq  11992  odd2np1lem  12016  oddp1even  12020  opoe  12039  m1expo  12044  m1exp1  12045  nn0o1gt2  12049  nninfdcex  12093  gcddvds  12103  gcdcl  12106  gcdeq0  12117  gcd0id  12119  bezoutr1  12173  nnmindc  12174  nnminle  12175  eucalg  12200  lcm0val  12206  lcmid  12221  rpmul  12239  dfphi2  12361  phiprmpw  12363  hashgcdeq  12380  odzdvds  12386  nnnn0modprm0  12396  pythagtriplem4  12409  pythagtriplem12  12416  pcaddlem  12480  pcmpt  12484  pockthi  12499  4sqlem12  12543  ennnfonelem0  12565  ennnfonelem1  12567  ennnfonelemhdmp1  12569  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemf1  12578  ctiunctlemfo  12599  setsresg  12659  strressid  12692  strle1g  12727  restid2  12862  gsumwmhm  13073  grplactcnv  13177  mulg0  13198  mulgnn0gsum  13201  mulgneg  13213  mulgneg2  13229  gsumfzconst  13414  gsumfzsnfd  13418  gsumfzfsumlem0  14085  zrhval2  14118  tgval2  14230  tgidm  14253  epttop  14269  tgrest  14348  restco  14353  restsn  14359  tgcn  14387  cnptopresti  14417  cnptoprest  14418  txbas  14437  upxp  14451  txrest  14455  txdis  14456  txhmeo  14498  txswaphmeolem  14499  xblss2ps  14583  xblss2  14584  qtopbasss  14700  fsumcncntop  14746  hoverb  14827  limcimolemlt  14843  dvcnp2cntop  14878  dvcoapbr  14886  dvexp  14890  dvexp2  14891  dvmptid  14895  dveflem  14905  dvef  14906  plymullem1  14927  plyadd  14930  plymul  14931  plycjlemc  14938  plycj  14939  sin0pilem1  14957  sin2kpi  14987  cos2kpi  14988  coseq0q4123  15010  coseq0negpitopi  15012  sincosq1eq  15015  sinkpi  15023  coskpi  15024  1cxp  15076  lgslem2  15158  lgsfcl2  15163  lgs0  15170  lgs2  15174  lgsneg  15181  lgsdilem  15184  lgsdir2lem4  15188  lgsdir2lem5  15189  lgsne0  15195  lgssq  15197  lgssq2  15198  gausslemma2dlem3  15220  gausslemma2dlem4  15221  lgseisenlem1  15227  lgsquadlem2  15235  lgsquad2lem2  15239  lgsquad3  15241  m1lgs  15242  2lgslem1a2  15244  2lgsoddprmlem3  15268  2sqlem9  15281  2sqlem10  15282  ex-ceil  15288  bj-intexr  15470  peano3nninf  15567  nninfall  15569  isomninnlem  15590  iswomni0  15611  ismkvnnlem  15612  nconstwlpolem0  15623