Theorem eqtrdi 2226

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtr2di  2227  eqtr4di  2228  3eqtr3g  2233  3eqtr4a  2236  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  csbprc  3468  un00  3469  disjssun  3486  disjpr2  3656  tppreq3  3695  diftpsn3  3733  preq12b  3770  intsng  3878  uniintsnr  3880  rint0  3883  riin0  3958  iununir  3970  intexr  4150  exmid1stab  4208  sucprc  4412  op1stbg  4479  elreldm  4853  xpeq0r  5051  xpdisj1  5053  xpdisj2  5054  resdisj  5057  xpima1  5075  xpima2m  5076  elxp4  5116  unixp0im  5165  uniabio  5188  iotass  5195  cnvresid  5290  funimacnv  5292  f1o00  5496  dffv4g  5512  fnrnfv  5562  feqresmpt  5570  dffn5imf  5571  funfvdm2f  5581  fvun1  5582  fvmpt2  5599  fndmin  5623  fmptcof  5683  fmptcos  5684  fvunsng  5710  fvpr1  5720  fnrnov  6019  offval  6089  ofrfval  6090  op1std  6148  op2ndd  6149  fmpoco  6216  tpostpos  6264  tfr0  6323  rdgival  6382  frec0g  6397  2oconcl  6439  om0  6458  oei0  6459  oasuc  6464  omv2  6465  nnm0r  6479  uniqs2  6594  en1  6798  en1bg  6799  fundmen  6805  mapsnen  6810  xpsnen  6820  xpcomco  6825  xpdom2  6830  xpmapenlem  6848  exmidpweq  6908  unsnfidcex  6918  fiintim  6927  ssfirab  6932  sbthlemi8  6962  elfi2  6970  fi0  6973  fieq0  6974  djudom  7091  ismkvnex  7152  nninfwlpoimlemg  7172  en2other2  7194  exmidfodomrlemim  7199  nq0m0r  7454  addpinq1  7462  genipv  7507  genpelvl  7510  genpelvu  7511  cauappcvgprlem1  7657  caucvgsrlemoffres  7798  addresr  7835  mulresr  7836  axcnre  7879  add20  8429  rimul  8540  rereim  8541  mulreim  8559  sup3exmid  8912  fv0p1e1  9032  div4p1lem1div2  9170  nnm1nn0  9215  znegcl  9282  peano2z  9287  nneoor  9353  nn0ind-raph  9368  xnegneg  9831  xltnegi  9833  xaddpnf1  9844  xnegid  9857  xnn0xadd0  9865  xnegdi  9866  xsubge0  9879  xposdif  9880  xlesubadd  9881  xleaddadd  9885  fz0to4untppr  10121  fzo0to2pr  10215  fldiv4p1lem1div2  10302  mulp1mod1  10362  frecfzennn  10423  iseqf1olemqk  10491  exp0  10521  expp1  10524  expnegap0  10525  1exp  10546  mulexp  10556  m1expeven  10564  sq0i  10608  bernneq  10637  facp1  10705  faclbnd3  10718  facubnd  10720  bcval5  10738  hashinfom  10753  hashsng  10773  hashxp  10801  resunimafz0  10806  zfz1iso  10816  imre  10855  reim0b  10866  rereb  10867  resqrexlemover  11014  resqrexlemcalc1  11018  abs00bd  11070  maxabslemlub  11211  xrmaxiflemcom  11252  xrmaxadd  11264  climconst  11293  isumz  11392  fsumf1o  11393  fsumcllem  11402  fsumadd  11409  fsumxp  11439  fsumcnv  11440  fsummulc2  11451  fsumconst  11457  fsumabs  11468  telfsumo  11469  fsumparts  11473  fsumrelem  11474  fsumiun  11480  binomlem  11486  binom  11487  binom11  11489  isumsplit  11494  arisum  11501  arisum2  11502  trireciplem  11503  georeclim  11516  cvgratnnlemseq  11529  prodfrecap  11549  prod1dc  11589  fprodf1o  11591  fprodcl2lem  11608  fprodcllem  11609  fprodfac  11618  fprod2d  11626  fprodxp  11627  fprodcnv  11628  fprodrec  11632  fprodmodd  11644  ef0lem  11663  ege2le3  11674  efaddlem  11677  efcan  11679  eft0val  11696  ef4p  11697  efgt1p2  11698  efi4p  11720  sincossq  11751  cos2tsin  11754  absefi  11771  demoivreALT  11776  p1modz1  11796  dvdsabseq  11847  odd2np1lem  11871  oddp1even  11875  opoe  11894  m1expo  11899  m1exp1  11900  nn0o1gt2  11904  nninfdcex  11948  gcddvds  11958  gcdcl  11961  gcdeq0  11972  gcd0id  11974  bezoutr1  12028  nnmindc  12029  nnminle  12030  eucalg  12053  lcm0val  12059  lcmid  12074  rpmul  12092  dfphi2  12214  phiprmpw  12216  hashgcdeq  12233  odzdvds  12239  nnnn0modprm0  12249  pythagtriplem4  12262  pythagtriplem12  12269  pcaddlem  12332  pcmpt  12335  pockthi  12350  ennnfonelem0  12400  ennnfonelem1  12402  ennnfonelemhdmp1  12404  ennnfonelemkh  12407  ennnfonelemhf1o  12408  ennnfonelemf1  12413  ctiunctlemfo  12434  setsresg  12494  strressid  12524  strle1g  12559  restid2  12687  grplactcnv  12926  mulg0  12942  mulgneg  12955  mulgneg2  12970  tgval2  13444  tgidm  13467  epttop  13483  tgrest  13562  restco  13567  restsn  13573  tgcn  13601  cnptopresti  13631  cnptoprest  13632  txbas  13651  upxp  13665  txrest  13669  txdis  13670  txhmeo  13712  txswaphmeolem  13713  xblss2ps  13797  xblss2  13798  qtopbasss  13914  fsumcncntop  13949  limcimolemlt  14026  dvcnp2cntop  14056  dvcoapbr  14064  dvexp  14068  dvexp2  14069  dveflem  14080  dvef  14081  sin0pilem1  14095  sin2kpi  14125  cos2kpi  14126  coseq0q4123  14148  coseq0negpitopi  14150  sincosq1eq  14153  sinkpi  14161  coskpi  14162  1cxp  14214  lgslem2  14295  lgsfcl2  14300  lgs0  14307  lgs2  14311  lgsneg  14318  lgsdilem  14321  lgsdir2lem4  14325  lgsdir2lem5  14326  lgsne0  14332  lgssq  14334  lgssq2  14335  2sqlem9  14353  2sqlem10  14354  ex-ceil  14360  bj-intexr  14542  peano3nninf  14638  nninfall  14640  isomninnlem  14660  iswomni0  14681  ismkvnnlem  14682  nconstwlpolem0  14692