Theorem eqtrdi 2287

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2di  2288  eqtr4di  2289  3eqtr3g  2294  3eqtr4a  2297  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  un00  3567  vvin  3569  csbprc  3572  disjssun  3588  disjpr2  3773  tppreq3  3814  diftpsn3  3856  ssprsseq  3877  preq12b  3895  intsng  4004  uniintsnr  4006  rint0  4009  riin0  4084  iununir  4096  intexr  4288  exmid1stab  4347  sucprc  4559  op1stbg  4627  elreldm  5010  xpeq0r  5213  xpdisj1  5215  xpdisj2  5216  resdisj  5219  xpima1  5237  xpima2m  5238  elxp4  5278  unixp0im  5327  uniabio  5351  iotass  5358  cnvresid  5458  funimacnv  5460  fresaunres2disj  5573  fimadmfo  5627  f1o00  5679  dffv4g  5695  fv2prc  5738  fnrnfv  5752  feqresmpt  5760  dffn5imf  5761  funfvdm2f  5771  fvun1  5772  fvmpt2  5792  fndmin  5819  fmptcof  5878  fmptcos  5879  funopdmsn  5898  fvunsng  5912  fvpr1  5922  dfimafnf  5958  fnrnov  6238  f1o3d  6301  offval  6314  ofrfval  6315  op1std  6386  op2ndd  6387  fmpoco  6456  suppsnopdc  6494  mptsuppdifd  6499  supp0cosupp0fn  6511  tpostpos  6539  tfr0  6598  rdgival  6657  frec0g  6672  2oconcl  6716  om0  6735  oei0  6736  oasuc  6741  omv2  6742  nnm0r  6756  uniqs2  6873  en1  7090  en1bg  7091  fundmen  7098  mapsnen  7104  en2  7116  xpsnen  7123  xpcomco  7128  xpdom2  7133  xpmapenlem  7153  exmidpweq  7220  unsnfidcex  7231  fiintim  7242  ssfirab  7248  sbthlemi8  7286  elfi2  7311  fi0  7314  fieq0  7315  djudom  7439  ismkvnex  7501  nninfwlpoimlemg  7521  en2other2  7554  exmidfodomrlemim  7559  nq0m0r  7829  addpinq1  7837  genipv  7882  genpelvl  7885  genpelvu  7886  cauappcvgprlem1  8032  caucvgsrlemoffres  8173  addresr  8210  mulresr  8211  axcnre  8254  add20  8809  rimul  8921  rereim  8922  mulreim  8940  sup3exmid  9295  fv0p1e1  9428  div4p1lem1div2  9570  nnm1nn0  9615  znegcl  9686  peano2z  9691  nneoor  9759  nn0ind-raph  9774  xnegneg  10252  xltnegi  10254  xaddpnf1  10265  xnegid  10278  xnn0xadd0  10286  xnegdi  10287  xsubge0  10300  xposdif  10301  xlesubadd  10302  xleaddadd  10306  fz0to4untppr  10548  fzo0to2pr  10653  nninfdcex  10689  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  mulp1mod1  10823  frecfzennn  10884  iseqf1olemqk  10965  exp0  11001  expp1  11004  expnegap0  11005  1exp  11026  mulexp  11036  m1expeven  11044  sq0i  11089  bernneq  11119  facp1  11190  faclbnd3  11203  facubnd  11205  bcval5  11223  hashinfom  11239  hashsng  11259  hashxp  11289  hashpwfi  11291  resunimafz0  11296  ssenneg  11302  hashfibclem  11304  hashfibc  11305  hashf1lem2  11308  hashf1  11309  zfz1iso  11315  hash2en  11317  hashtpgim  11319  lsw1  11376  s1rn  11408  eqs1  11418  ccat1st1st  11431  swrd00g  11443  swrdlend  11452  swrds1  11462  cats1lend  11561  cats2catd  11563  s2leng  11583  s2dmg  11584  imre  11638  reim0b  11649  rereb  11650  sq01  11682  resqrexlemover  11798  resqrexlemcalc1  11802  abs00bd  11854  maxabslemlub  11996  xrmaxiflemcom  12040  xrmaxadd  12052  climconst  12081  fzf1o  12167  isumz  12181  fsumf1o  12182  fsumcllem  12191  fsumadd  12198  fsumxp  12228  fsumcnv  12229  fsummulc2  12240  fsumconst  12246  fsumabs  12257  telfsumo  12258  fsumparts  12262  fsumrelem  12263  fsumiun  12269  binomlem  12275  binom  12276  binom11  12278  isumsplit  12283  arisum  12290  arisum2  12291  trireciplem  12292  georeclim  12305  cvgratnnlemseq  12318  prodfrecap  12338  prod1dc  12378  fprodf1o  12380  fprodcl2lem  12397  fprodcllem  12398  fprodfac  12407  fprod2d  12415  fprodxp  12416  fprodcnv  12417  fprodrec  12421  fprodmodd  12433  ef0lem  12452  ege2le3  12463  efaddlem  12466  efcan  12468  eft0val  12485  ef4p  12486  efgt1p2  12487  efi4p  12509  sincossq  12540  cos2tsin  12543  absefi  12561  demoivreALT  12566  p1modz1  12586  dvdsabseq  12639  odd2np1lem  12664  oddp1even  12668  opoe  12687  m1expo  12692  m1exp1  12693  nn0o1gt2  12697  bitsinv1  12754  gcddvds  12765  gcdcl  12768  gcdeq0  12779  gcd0id  12781  bezoutr1  12835  nnmindc  12836  nnminle  12837  eucalg  12862  lcm0val  12868  lcmid  12883  rpmul  12901  dfphi2  13027  phiprmpw  13029  hashgcdeq  13047  odzdvds  13053  nnnn0modprm0  13063  pythagtriplem4  13076  pythagtriplem12  13083  pcaddlem  13147  pcmpt  13151  pockthi  13166  4sqlem12  13210  2expltfac  13248  prmlem0  13249  ballotfilemfp1  13289  ballotfilemfval0  13293  ballotfilemsv  13311  ennnfonelem0  13354  ennnfonelem1  13356  ennnfonelemhdmp1  13358  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemf1  13367  ctiunctlemfo  13388  setsresg  13448  strressid  13484  strle1g  13519  restid2  13661  gzsumwmhm  13862  grplactcnv  13966  mulg0  13987  mulgnn0gzsum  13990  mulgneg  14002  mulgneg2  14018  gzsumconst  14233  gzsumsnfd  14237  gzsumsplit0  14238  gsumvalfi  14242  gsumsncmn  14246  gsump1  14247  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsumresfi  14263  gsummhmfi  14264  gsum2dfilem2  14272  gsum2dfi  14273  gsum2d2fi  14274  gsumcom2fi  14275  prdsbas3  14294  zrhval2  15063  assamulgscmlem2  15151  mpl0fi  15218  tgval2  15277  tgidm  15300  epttop  15316  tgrest  15395  restco  15400  restsn  15406  tgcn  15434  cnptopresti  15464  cnptoprest  15465  txbas  15484  upxp  15498  txrest  15502  txdis  15503  txhmeo  15545  txswaphmeolem  15546  xblss2ps  15630  xblss2  15631  qtopbasss  15747  fsumcncntop  15793  hoverb  15874  limcimolemlt  15890  dvcnp2cntop  15925  dvcoapbr  15933  dvexp  15937  dvexp2  15938  dvmptid  15942  dveflem  15952  dvef  15953  plymullem1  15974  plyadd  15977  plymul  15978  plycoeid3  15983  plycjlemc  15986  plycj  15987  sin0pilem1  16008  sin2kpi  16038  cos2kpi  16039  coseq0q4123  16061  coseq0negpitopi  16063  sincosq1eq  16066  sinkpi  16074  coskpi  16075  sineq0re  16076  root1idef  16084  logfac  16126  1cxp  16133  birthdaylem2  16226  birthdaylem3  16227  efnnfsumcl  16239  ppiprm  16259  chtprm  16261  chtdif  16264  efchtqdvds  16265  ppidif  16269  ppiqltx  16281  prmorcht  16282  mpodvdsmulf1o  16284  chtublem  16295  chtqub  16296  bclbnd  16307  bposlem1  16311  bposlem2  16312  bposlem5  16315  bposlem6  16316  bposlem8  16318  bposlem9  16319  lgslem2  16325  lgsfcl2  16330  lgs0  16337  lgs2  16341  lgsneg  16348  lgsdilem  16351  lgsdir2lem4  16355  lgsdir2lem5  16356  lgsne0  16362  lgssq  16364  lgssq2  16365  gausslemma2dlem3  16387  gausslemma2dlem4  16388  lgseisenlem1  16394  lgsquadlem2  16402  lgsquad2lem2  16406  lgsquad3  16408  m1lgs  16409  2lgslem1a2  16411  2lgsoddprmlem3  16435  2sqlem9  16448  2sqlem10  16449  edgiedgbg  16511  isuhgrm  16517  isushgrm  16518  uhgr0vb  16530  uhgrun  16532  isupgren  16541  isumgren  16551  umgrnloop0  16563  upgrun  16572  umgrun  16574  isuspgren  16603  isusgren  16604  usgrf1oedg  16651  usgredg3  16660  egrsubgr  16709  0uhgrsubgr  16711  uhgrspansubgrlem  16722  vtxdg0v  16740  vtxdgfi0e  16741  vtxdfifiun  16743  vtxdumgrfival  16744  1loopgrvd2fi  16751  vdegp1cid  16762  wlkl1loop  16804  2wlklem  16822  upgr2wlkdc  16823  clwwlkn0  16854  clwwlkn1  16864  clwwlkn2  16867  umgr2cwwk2dif  16870  clwwlk0on0  16877  clwwlknonel  16878  clwwlknonex2lem1  16883  trlsegvdeglem4  16909  eupthvdres  16921  eupth2lembfi  16923  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  ex-ceil  16945  bj-intexr  17139  wexmiddiffilem  17248  wexmiddifxylem  17250  peano3nninf  17256  nninfall  17258  isomninnlem  17285  iswomni0  17308  ismkvnnlem  17309  nconstwlpolem0  17320