Theorem eqtrdi 2245

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 2229	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtr2di  2246  eqtr4di  2247  3eqtr3g  2252  3eqtr4a  2255  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  csbprc  3497  un00  3498  disjssun  3515  disjpr2  3687  tppreq3  3726  diftpsn3  3764  preq12b  3801  intsng  3909  uniintsnr  3911  rint0  3914  riin0  3989  iununir  4001  intexr  4184  exmid1stab  4242  sucprc  4448  op1stbg  4515  elreldm  4893  xpeq0r  5093  xpdisj1  5095  xpdisj2  5096  resdisj  5099  xpima1  5117  xpima2m  5118  elxp4  5158  unixp0im  5207  uniabio  5230  iotass  5237  cnvresid  5333  funimacnv  5335  fimadmfo  5492  f1o00  5542  dffv4g  5558  fv2prc  5598  fnrnfv  5610  feqresmpt  5618  dffn5imf  5619  funfvdm2f  5629  fvun1  5630  fvmpt2  5648  fndmin  5672  fmptcof  5732  fmptcos  5733  fvunsng  5759  fvpr1  5769  fnrnov  6073  offval  6147  ofrfval  6148  op1std  6215  op2ndd  6216  fmpoco  6283  tpostpos  6331  tfr0  6390  rdgival  6449  frec0g  6464  2oconcl  6506  om0  6525  oei0  6526  oasuc  6531  omv2  6532  nnm0r  6546  uniqs2  6663  en1  6867  en1bg  6868  fundmen  6874  mapsnen  6879  xpsnen  6889  xpcomco  6894  xpdom2  6899  xpmapenlem  6919  exmidpweq  6979  unsnfidcex  6990  fiintim  7001  ssfirab  7006  sbthlemi8  7039  elfi2  7047  fi0  7050  fieq0  7051  djudom  7168  ismkvnex  7230  nninfwlpoimlemg  7250  en2other2  7277  exmidfodomrlemim  7282  nq0m0r  7542  addpinq1  7550  genipv  7595  genpelvl  7598  genpelvu  7599  cauappcvgprlem1  7745  caucvgsrlemoffres  7886  addresr  7923  mulresr  7924  axcnre  7967  add20  8520  rimul  8631  rereim  8632  mulreim  8650  sup3exmid  9003  fv0p1e1  9124  div4p1lem1div2  9264  nnm1nn0  9309  znegcl  9376  peano2z  9381  nneoor  9447  nn0ind-raph  9462  xnegneg  9927  xltnegi  9929  xaddpnf1  9940  xnegid  9953  xnn0xadd0  9961  xnegdi  9962  xsubge0  9975  xposdif  9976  xlesubadd  9977  xleaddadd  9981  fz0to4untppr  10218  fzo0to2pr  10313  nninfdcex  10346  fldiv4p1lem1div2  10414  fldiv4lem1div2  10416  mulp1mod1  10476  frecfzennn  10537  iseqf1olemqk  10618  exp0  10654  expp1  10657  expnegap0  10658  1exp  10679  mulexp  10689  m1expeven  10697  sq0i  10742  bernneq  10771  facp1  10841  faclbnd3  10854  facubnd  10856  bcval5  10874  hashinfom  10889  hashsng  10909  hashxp  10937  resunimafz0  10942  zfz1iso  10952  imre  11035  reim0b  11046  rereb  11047  resqrexlemover  11194  resqrexlemcalc1  11198  abs00bd  11250  maxabslemlub  11391  xrmaxiflemcom  11433  xrmaxadd  11445  climconst  11474  isumz  11573  fsumf1o  11574  fsumcllem  11583  fsumadd  11590  fsumxp  11620  fsumcnv  11621  fsummulc2  11632  fsumconst  11638  fsumabs  11649  telfsumo  11650  fsumparts  11654  fsumrelem  11655  fsumiun  11661  binomlem  11667  binom  11668  binom11  11670  isumsplit  11675  arisum  11682  arisum2  11683  trireciplem  11684  georeclim  11697  cvgratnnlemseq  11710  prodfrecap  11730  prod1dc  11770  fprodf1o  11772  fprodcl2lem  11789  fprodcllem  11790  fprodfac  11799  fprod2d  11807  fprodxp  11808  fprodcnv  11809  fprodrec  11813  fprodmodd  11825  ef0lem  11844  ege2le3  11855  efaddlem  11858  efcan  11860  eft0val  11877  ef4p  11878  efgt1p2  11879  efi4p  11901  sincossq  11932  cos2tsin  11935  absefi  11953  demoivreALT  11958  p1modz1  11978  dvdsabseq  12031  odd2np1lem  12056  oddp1even  12060  opoe  12079  m1expo  12084  m1exp1  12085  nn0o1gt2  12089  bitsinv1  12146  gcddvds  12157  gcdcl  12160  gcdeq0  12171  gcd0id  12173  bezoutr1  12227  nnmindc  12228  nnminle  12229  eucalg  12254  lcm0val  12260  lcmid  12275  rpmul  12293  dfphi2  12415  phiprmpw  12417  hashgcdeq  12435  odzdvds  12441  nnnn0modprm0  12451  pythagtriplem4  12464  pythagtriplem12  12471  pcaddlem  12535  pcmpt  12539  pockthi  12554  4sqlem12  12598  2expltfac  12635  ennnfonelem0  12649  ennnfonelem1  12651  ennnfonelemhdmp1  12653  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemf1  12662  ctiunctlemfo  12683  setsresg  12743  strressid  12776  strle1g  12811  restid2  12952  prdsbas3  12991  gsumwmhm  13202  grplactcnv  13306  mulg0  13333  mulgnn0gsum  13336  mulgneg  13348  mulgneg2  13364  gsumfzconst  13549  gsumfzsnfd  13553  gsumfzfsumlem0  14220  zrhval2  14253  mpl0fi  14336  tgval2  14395  tgidm  14418  epttop  14434  tgrest  14513  restco  14518  restsn  14524  tgcn  14552  cnptopresti  14582  cnptoprest  14583  txbas  14602  upxp  14616  txrest  14620  txdis  14621  txhmeo  14663  txswaphmeolem  14664  xblss2ps  14748  xblss2  14749  qtopbasss  14865  fsumcncntop  14911  hoverb  14992  limcimolemlt  15008  dvcnp2cntop  15043  dvcoapbr  15051  dvexp  15055  dvexp2  15056  dvmptid  15060  dveflem  15070  dvef  15071  plymullem1  15092  plyadd  15095  plymul  15096  plycoeid3  15101  plycjlemc  15104  plycj  15105  sin0pilem1  15125  sin2kpi  15155  cos2kpi  15156  coseq0q4123  15178  coseq0negpitopi  15180  sincosq1eq  15183  sinkpi  15191  coskpi  15192  1cxp  15244  mpodvdsmulf1o  15334  lgslem2  15350  lgsfcl2  15355  lgs0  15362  lgs2  15366  lgsneg  15373  lgsdilem  15376  lgsdir2lem4  15380  lgsdir2lem5  15381  lgsne0  15387  lgssq  15389  lgssq2  15390  gausslemma2dlem3  15412  gausslemma2dlem4  15413  lgseisenlem1  15419  lgsquadlem2  15427  lgsquad2lem2  15431  lgsquad3  15433  m1lgs  15434  2lgslem1a2  15436  2lgsoddprmlem3  15460  2sqlem9  15473  2sqlem10  15474  ex-ceil  15480  bj-intexr  15662  peano3nninf  15762  nninfall  15764  isomninnlem  15787  iswomni0  15808  ismkvnnlem  15809  nconstwlpolem0  15820