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  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  csbprc  3492  un00  3493  disjssun  3510  disjpr2  3682  tppreq3  3721  diftpsn3  3759  preq12b  3796  intsng  3904  uniintsnr  3906  rint0  3909  riin0  3984  iununir  3996  intexr  4179  exmid1stab  4237  sucprc  4443  op1stbg  4510  elreldm  4888  xpeq0r  5088  xpdisj1  5090  xpdisj2  5091  resdisj  5094  xpima1  5112  xpima2m  5113  elxp4  5153  unixp0im  5202  uniabio  5225  iotass  5232  cnvresid  5328  funimacnv  5330  fimadmfo  5485  f1o00  5535  dffv4g  5551  fv2prc  5591  fnrnfv  5603  feqresmpt  5611  dffn5imf  5612  funfvdm2f  5622  fvun1  5623  fvmpt2  5641  fndmin  5665  fmptcof  5725  fmptcos  5726  fvunsng  5752  fvpr1  5762  fnrnov  6064  offval  6138  ofrfval  6139  op1std  6201  op2ndd  6202  fmpoco  6269  tpostpos  6317  tfr0  6376  rdgival  6435  frec0g  6450  2oconcl  6492  om0  6511  oei0  6512  oasuc  6517  omv2  6518  nnm0r  6532  uniqs2  6649  en1  6853  en1bg  6854  fundmen  6860  mapsnen  6865  xpsnen  6875  xpcomco  6880  xpdom2  6885  xpmapenlem  6905  exmidpweq  6965  unsnfidcex  6976  fiintim  6985  ssfirab  6990  sbthlemi8  7023  elfi2  7031  fi0  7034  fieq0  7035  djudom  7152  ismkvnex  7214  nninfwlpoimlemg  7234  en2other2  7256  exmidfodomrlemim  7261  nq0m0r  7516  addpinq1  7524  genipv  7569  genpelvl  7572  genpelvu  7573  cauappcvgprlem1  7719  caucvgsrlemoffres  7860  addresr  7897  mulresr  7898  axcnre  7941  add20  8493  rimul  8604  rereim  8605  mulreim  8623  sup3exmid  8976  fv0p1e1  9097  div4p1lem1div2  9236  nnm1nn0  9281  znegcl  9348  peano2z  9353  nneoor  9419  nn0ind-raph  9434  xnegneg  9899  xltnegi  9901  xaddpnf1  9912  xnegid  9925  xnn0xadd0  9933  xnegdi  9934  xsubge0  9947  xposdif  9948  xlesubadd  9949  xleaddadd  9953  fz0to4untppr  10190  fzo0to2pr  10285  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  mulp1mod1  10436  frecfzennn  10497  iseqf1olemqk  10578  exp0  10614  expp1  10617  expnegap0  10618  1exp  10639  mulexp  10649  m1expeven  10657  sq0i  10702  bernneq  10731  facp1  10801  faclbnd3  10814  facubnd  10816  bcval5  10834  hashinfom  10849  hashsng  10869  hashxp  10897  resunimafz0  10902  zfz1iso  10912  imre  10995  reim0b  11006  rereb  11007  resqrexlemover  11154  resqrexlemcalc1  11158  abs00bd  11210  maxabslemlub  11351  xrmaxiflemcom  11392  xrmaxadd  11404  climconst  11433  isumz  11532  fsumf1o  11533  fsumcllem  11542  fsumadd  11549  fsumxp  11579  fsumcnv  11580  fsummulc2  11591  fsumconst  11597  fsumabs  11608  telfsumo  11609  fsumparts  11613  fsumrelem  11614  fsumiun  11620  binomlem  11626  binom  11627  binom11  11629  isumsplit  11634  arisum  11641  arisum2  11642  trireciplem  11643  georeclim  11656  cvgratnnlemseq  11669  prodfrecap  11689  prod1dc  11729  fprodf1o  11731  fprodcl2lem  11748  fprodcllem  11749  fprodfac  11758  fprod2d  11766  fprodxp  11767  fprodcnv  11768  fprodrec  11772  fprodmodd  11784  ef0lem  11803  ege2le3  11814  efaddlem  11817  efcan  11819  eft0val  11836  ef4p  11837  efgt1p2  11838  efi4p  11860  sincossq  11891  cos2tsin  11894  absefi  11912  demoivreALT  11917  p1modz1  11937  dvdsabseq  11989  odd2np1lem  12013  oddp1even  12017  opoe  12036  m1expo  12041  m1exp1  12042  nn0o1gt2  12046  nninfdcex  12090  gcddvds  12100  gcdcl  12103  gcdeq0  12114  gcd0id  12116  bezoutr1  12170  nnmindc  12171  nnminle  12172  eucalg  12197  lcm0val  12203  lcmid  12218  rpmul  12236  dfphi2  12358  phiprmpw  12360  hashgcdeq  12377  odzdvds  12383  nnnn0modprm0  12393  pythagtriplem4  12406  pythagtriplem12  12413  pcaddlem  12477  pcmpt  12481  pockthi  12496  4sqlem12  12540  ennnfonelem0  12562  ennnfonelem1  12564  ennnfonelemhdmp1  12566  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemf1  12575  ctiunctlemfo  12596  setsresg  12656  strressid  12689  strle1g  12724  restid2  12859  gsumwmhm  13070  grplactcnv  13174  mulg0  13195  mulgnn0gsum  13198  mulgneg  13210  mulgneg2  13226  gsumfzconst  13411  gsumfzsnfd  13415  gsumfzfsumlem0  14074  zrhval2  14107  tgval2  14219  tgidm  14242  epttop  14258  tgrest  14337  restco  14342  restsn  14348  tgcn  14376  cnptopresti  14406  cnptoprest  14407  txbas  14426  upxp  14440  txrest  14444  txdis  14445  txhmeo  14487  txswaphmeolem  14488  xblss2ps  14572  xblss2  14573  qtopbasss  14689  fsumcncntop  14724  hoverb  14802  limcimolemlt  14818  dvcnp2cntop  14848  dvcoapbr  14856  dvexp  14860  dvexp2  14861  dveflem  14872  dvef  14873  plymullem1  14894  plyadd  14897  plymul  14898  sin0pilem1  14916  sin2kpi  14946  cos2kpi  14947  coseq0q4123  14969  coseq0negpitopi  14971  sincosq1eq  14974  sinkpi  14982  coskpi  14983  1cxp  15035  lgslem2  15117  lgsfcl2  15122  lgs0  15129  lgs2  15133  lgsneg  15140  lgsdilem  15143  lgsdir2lem4  15147  lgsdir2lem5  15148  lgsne0  15154  lgssq  15156  lgssq2  15157  gausslemma2dlem3  15179  gausslemma2dlem4  15180  lgseisenlem1  15186  m1lgs  15192  2lgsoddprmlem3  15199  2sqlem9  15211  2sqlem10  15212  ex-ceil  15218  bj-intexr  15400  peano3nninf  15497  nninfall  15499  isomninnlem  15520  iswomni0  15541  ismkvnnlem  15542  nconstwlpolem0  15553