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  7275  exmidfodomrlemim  7280  nq0m0r  7540  addpinq1  7548  genipv  7593  genpelvl  7596  genpelvu  7597  cauappcvgprlem1  7743  caucvgsrlemoffres  7884  addresr  7921  mulresr  7922  axcnre  7965  add20  8518  rimul  8629  rereim  8630  mulreim  8648  sup3exmid  9001  fv0p1e1  9122  div4p1lem1div2  9262  nnm1nn0  9307  znegcl  9374  peano2z  9379  nneoor  9445  nn0ind-raph  9460  xnegneg  9925  xltnegi  9927  xaddpnf1  9938  xnegid  9951  xnn0xadd0  9959  xnegdi  9960  xsubge0  9973  xposdif  9974  xlesubadd  9975  xleaddadd  9979  fz0to4untppr  10216  fzo0to2pr  10311  nninfdcex  10344  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  mulp1mod1  10474  frecfzennn  10535  iseqf1olemqk  10616  exp0  10652  expp1  10655  expnegap0  10656  1exp  10677  mulexp  10687  m1expeven  10695  sq0i  10740  bernneq  10769  facp1  10839  faclbnd3  10852  facubnd  10854  bcval5  10872  hashinfom  10887  hashsng  10907  hashxp  10935  resunimafz0  10940  zfz1iso  10950  imre  11033  reim0b  11044  rereb  11045  resqrexlemover  11192  resqrexlemcalc1  11196  abs00bd  11248  maxabslemlub  11389  xrmaxiflemcom  11431  xrmaxadd  11443  climconst  11472  isumz  11571  fsumf1o  11572  fsumcllem  11581  fsumadd  11588  fsumxp  11618  fsumcnv  11619  fsummulc2  11630  fsumconst  11636  fsumabs  11647  telfsumo  11648  fsumparts  11652  fsumrelem  11653  fsumiun  11659  binomlem  11665  binom  11666  binom11  11668  isumsplit  11673  arisum  11680  arisum2  11681  trireciplem  11682  georeclim  11695  cvgratnnlemseq  11708  prodfrecap  11728  prod1dc  11768  fprodf1o  11770  fprodcl2lem  11787  fprodcllem  11788  fprodfac  11797  fprod2d  11805  fprodxp  11806  fprodcnv  11807  fprodrec  11811  fprodmodd  11823  ef0lem  11842  ege2le3  11853  efaddlem  11856  efcan  11858  eft0val  11875  ef4p  11876  efgt1p2  11877  efi4p  11899  sincossq  11930  cos2tsin  11933  absefi  11951  demoivreALT  11956  p1modz1  11976  dvdsabseq  12029  odd2np1lem  12054  oddp1even  12058  opoe  12077  m1expo  12082  m1exp1  12083  nn0o1gt2  12087  bitsinv1  12144  gcddvds  12155  gcdcl  12158  gcdeq0  12169  gcd0id  12171  bezoutr1  12225  nnmindc  12226  nnminle  12227  eucalg  12252  lcm0val  12258  lcmid  12273  rpmul  12291  dfphi2  12413  phiprmpw  12415  hashgcdeq  12433  odzdvds  12439  nnnn0modprm0  12449  pythagtriplem4  12462  pythagtriplem12  12469  pcaddlem  12533  pcmpt  12537  pockthi  12552  4sqlem12  12596  2expltfac  12633  ennnfonelem0  12647  ennnfonelem1  12649  ennnfonelemhdmp1  12651  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemf1  12660  ctiunctlemfo  12681  setsresg  12741  strressid  12774  strle1g  12809  restid2  12950  prdsbas3  12989  gsumwmhm  13200  grplactcnv  13304  mulg0  13331  mulgnn0gsum  13334  mulgneg  13346  mulgneg2  13362  gsumfzconst  13547  gsumfzsnfd  13551  gsumfzfsumlem0  14218  zrhval2  14251  tgval2  14371  tgidm  14394  epttop  14410  tgrest  14489  restco  14494  restsn  14500  tgcn  14528  cnptopresti  14558  cnptoprest  14559  txbas  14578  upxp  14592  txrest  14596  txdis  14597  txhmeo  14639  txswaphmeolem  14640  xblss2ps  14724  xblss2  14725  qtopbasss  14841  fsumcncntop  14887  hoverb  14968  limcimolemlt  14984  dvcnp2cntop  15019  dvcoapbr  15027  dvexp  15031  dvexp2  15032  dvmptid  15036  dveflem  15046  dvef  15047  plymullem1  15068  plyadd  15071  plymul  15072  plycoeid3  15077  plycjlemc  15080  plycj  15081  sin0pilem1  15101  sin2kpi  15131  cos2kpi  15132  coseq0q4123  15154  coseq0negpitopi  15156  sincosq1eq  15159  sinkpi  15167  coskpi  15168  1cxp  15220  mpodvdsmulf1o  15310  lgslem2  15326  lgsfcl2  15331  lgs0  15338  lgs2  15342  lgsneg  15349  lgsdilem  15352  lgsdir2lem4  15356  lgsdir2lem5  15357  lgsne0  15363  lgssq  15365  lgssq2  15366  gausslemma2dlem3  15388  gausslemma2dlem4  15389  lgseisenlem1  15395  lgsquadlem2  15403  lgsquad2lem2  15407  lgsquad3  15409  m1lgs  15410  2lgslem1a2  15412  2lgsoddprmlem3  15436  2sqlem9  15449  2sqlem10  15450  ex-ceil  15456  bj-intexr  15638  peano3nninf  15738  nninfall  15740  isomninnlem  15761  iswomni0  15782  ismkvnnlem  15783  nconstwlpolem0  15794