Theorem eqtrdi 2238

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 2222	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 2171

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

This theorem is referenced by:  eqtr2di  2239  eqtr4di  2240  3eqtr3g  2245  3eqtr4a  2248  cbvralcsf  3138  cbvrexcsf  3139  cbvreucsf  3140  cbvrabcsf  3141  csbprc  3487  un00  3488  disjssun  3505  disjpr2  3678  tppreq3  3717  diftpsn3  3755  preq12b  3792  intsng  3900  uniintsnr  3902  rint0  3905  riin0  3980  iununir  3992  intexr  4175  exmid1stab  4233  sucprc  4437  op1stbg  4504  elreldm  4878  xpeq0r  5076  xpdisj1  5078  xpdisj2  5079  resdisj  5082  xpima1  5100  xpima2m  5101  elxp4  5141  unixp0im  5190  uniabio  5213  iotass  5220  cnvresid  5316  funimacnv  5318  f1o00  5522  dffv4g  5538  fv2prc  5578  fnrnfv  5590  feqresmpt  5598  dffn5imf  5599  funfvdm2f  5609  fvun1  5610  fvmpt2  5627  fndmin  5651  fmptcof  5711  fmptcos  5712  fvunsng  5738  fvpr1  5748  fnrnov  6050  offval  6122  ofrfval  6123  op1std  6181  op2ndd  6182  fmpoco  6249  tpostpos  6297  tfr0  6356  rdgival  6415  frec0g  6430  2oconcl  6472  om0  6491  oei0  6492  oasuc  6497  omv2  6498  nnm0r  6512  uniqs2  6629  en1  6833  en1bg  6834  fundmen  6840  mapsnen  6845  xpsnen  6855  xpcomco  6860  xpdom2  6865  xpmapenlem  6885  exmidpweq  6945  unsnfidcex  6956  fiintim  6965  ssfirab  6970  sbthlemi8  7002  elfi2  7010  fi0  7013  fieq0  7014  djudom  7131  ismkvnex  7193  nninfwlpoimlemg  7213  en2other2  7235  exmidfodomrlemim  7240  nq0m0r  7495  addpinq1  7503  genipv  7548  genpelvl  7551  genpelvu  7552  cauappcvgprlem1  7698  caucvgsrlemoffres  7839  addresr  7876  mulresr  7877  axcnre  7920  add20  8472  rimul  8583  rereim  8584  mulreim  8602  sup3exmid  8955  fv0p1e1  9075  div4p1lem1div2  9213  nnm1nn0  9258  znegcl  9325  peano2z  9330  nneoor  9396  nn0ind-raph  9411  xnegneg  9875  xltnegi  9877  xaddpnf1  9888  xnegid  9901  xnn0xadd0  9909  xnegdi  9910  xsubge0  9923  xposdif  9924  xlesubadd  9925  xleaddadd  9929  fz0to4untppr  10166  fzo0to2pr  10260  fldiv4p1lem1div2  10348  mulp1mod1  10408  frecfzennn  10469  iseqf1olemqk  10539  exp0  10570  expp1  10573  expnegap0  10574  1exp  10595  mulexp  10605  m1expeven  10613  sq0i  10658  bernneq  10687  facp1  10757  faclbnd3  10770  facubnd  10772  bcval5  10790  hashinfom  10805  hashsng  10825  hashxp  10853  resunimafz0  10858  zfz1iso  10868  imre  10907  reim0b  10918  rereb  10919  resqrexlemover  11066  resqrexlemcalc1  11070  abs00bd  11122  maxabslemlub  11263  xrmaxiflemcom  11304  xrmaxadd  11316  climconst  11345  isumz  11444  fsumf1o  11445  fsumcllem  11454  fsumadd  11461  fsumxp  11491  fsumcnv  11492  fsummulc2  11503  fsumconst  11509  fsumabs  11520  telfsumo  11521  fsumparts  11525  fsumrelem  11526  fsumiun  11532  binomlem  11538  binom  11539  binom11  11541  isumsplit  11546  arisum  11553  arisum2  11554  trireciplem  11555  georeclim  11568  cvgratnnlemseq  11581  prodfrecap  11601  prod1dc  11641  fprodf1o  11643  fprodcl2lem  11660  fprodcllem  11661  fprodfac  11670  fprod2d  11678  fprodxp  11679  fprodcnv  11680  fprodrec  11684  fprodmodd  11696  ef0lem  11715  ege2le3  11726  efaddlem  11729  efcan  11731  eft0val  11748  ef4p  11749  efgt1p2  11750  efi4p  11772  sincossq  11803  cos2tsin  11806  absefi  11823  demoivreALT  11828  p1modz1  11848  dvdsabseq  11900  odd2np1lem  11924  oddp1even  11928  opoe  11947  m1expo  11952  m1exp1  11953  nn0o1gt2  11957  nninfdcex  12001  gcddvds  12011  gcdcl  12014  gcdeq0  12025  gcd0id  12027  bezoutr1  12081  nnmindc  12082  nnminle  12083  eucalg  12108  lcm0val  12114  lcmid  12129  rpmul  12147  dfphi2  12269  phiprmpw  12271  hashgcdeq  12288  odzdvds  12294  nnnn0modprm0  12304  pythagtriplem4  12317  pythagtriplem12  12324  pcaddlem  12388  pcmpt  12392  pockthi  12407  4sqlem12  12451  ennnfonelem0  12473  ennnfonelem1  12475  ennnfonelemhdmp1  12477  ennnfonelemkh  12480  ennnfonelemhf1o  12481  ennnfonelemf1  12486  ctiunctlemfo  12507  setsresg  12567  strressid  12600  strle1g  12635  restid2  12770  grplactcnv  13077  mulg0  13098  mulgnn0gsum  13101  mulgneg  13113  mulgneg2  13129  zrhval2  13963  tgval2  14072  tgidm  14095  epttop  14111  tgrest  14190  restco  14195  restsn  14201  tgcn  14229  cnptopresti  14259  cnptoprest  14260  txbas  14279  upxp  14293  txrest  14297  txdis  14298  txhmeo  14340  txswaphmeolem  14341  xblss2ps  14425  xblss2  14426  qtopbasss  14542  fsumcncntop  14577  hoverb  14655  limcimolemlt  14671  dvcnp2cntop  14701  dvcoapbr  14709  dvexp  14713  dvexp2  14714  dveflem  14725  dvef  14726  sin0pilem1  14740  sin2kpi  14770  cos2kpi  14771  coseq0q4123  14793  coseq0negpitopi  14795  sincosq1eq  14798  sinkpi  14806  coskpi  14807  1cxp  14859  lgslem2  14941  lgsfcl2  14946  lgs0  14953  lgs2  14957  lgsneg  14964  lgsdilem  14967  lgsdir2lem4  14971  lgsdir2lem5  14972  lgsne0  14978  lgssq  14980  lgssq2  14981  lgseisenlem1  14989  m1lgs  14991  2lgsoddprmlem3  14998  2sqlem9  15010  2sqlem10  15011  ex-ceil  15017  bj-intexr  15199  peano3nninf  15296  nninfall  15298  isomninnlem  15319  iswomni0  15340  ismkvnnlem  15341  nconstwlpolem0  15352