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  4286  exmid1stab  4345  sucprc  4557  op1stbg  4625  elreldm  5008  xpeq0r  5210  xpdisj1  5212  xpdisj2  5213  resdisj  5216  xpima1  5234  xpima2m  5235  elxp4  5275  unixp0im  5324  uniabio  5348  iotass  5355  cnvresid  5455  funimacnv  5457  fresaunres2disj  5570  fimadmfo  5624  f1o00  5676  dffv4g  5692  fv2prc  5735  fnrnfv  5749  feqresmpt  5757  dffn5imf  5758  funfvdm2f  5768  fvun1  5769  fvmpt2  5789  fndmin  5816  fmptcof  5875  fmptcos  5876  funopdmsn  5895  fvunsng  5909  fvpr1  5919  dfimafnf  5955  fnrnov  6235  f1o3d  6298  offval  6310  ofrfval  6311  op1std  6382  op2ndd  6383  fmpoco  6452  suppsnopdc  6490  mptsuppdifd  6495  supp0cosupp0fn  6507  tpostpos  6535  tfr0  6594  rdgival  6653  frec0g  6668  2oconcl  6712  om0  6731  oei0  6732  oasuc  6737  omv2  6738  nnm0r  6752  uniqs2  6869  en1  7086  en1bg  7087  fundmen  7094  mapsnen  7100  en2  7112  xpsnen  7119  xpcomco  7124  xpdom2  7129  xpmapenlem  7149  exmidpweq  7216  unsnfidcex  7227  fiintim  7238  ssfirab  7244  sbthlemi8  7281  elfi2  7306  fi0  7309  fieq0  7310  djudom  7434  ismkvnex  7496  nninfwlpoimlemg  7516  en2other2  7549  exmidfodomrlemim  7554  nq0m0r  7824  addpinq1  7832  genipv  7877  genpelvl  7880  genpelvu  7881  cauappcvgprlem1  8027  caucvgsrlemoffres  8168  addresr  8205  mulresr  8206  axcnre  8249  add20  8804  rimul  8916  rereim  8917  mulreim  8935  sup3exmid  9290  fv0p1e1  9422  div4p1lem1div2  9564  nnm1nn0  9609  znegcl  9680  peano2z  9685  nneoor  9753  nn0ind-raph  9768  xnegneg  10246  xltnegi  10248  xaddpnf1  10259  xnegid  10272  xnn0xadd0  10280  xnegdi  10281  xsubge0  10294  xposdif  10295  xlesubadd  10296  xleaddadd  10300  fz0to4untppr  10542  fzo0to2pr  10647  nninfdcex  10683  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  mulp1mod1  10817  frecfzennn  10878  iseqf1olemqk  10959  exp0  10995  expp1  10998  expnegap0  10999  1exp  11020  mulexp  11030  m1expeven  11038  sq0i  11083  bernneq  11113  facp1  11184  faclbnd3  11197  facubnd  11199  bcval5  11217  hashinfom  11233  hashsng  11253  hashxp  11283  hashpwfi  11285  resunimafz0  11290  ssenneg  11296  hashfibclem  11298  hashfibc  11299  hashf1lem2  11302  hashf1  11303  zfz1iso  11309  hash2en  11311  hashtpgim  11313  lsw1  11370  s1rn  11402  eqs1  11412  ccat1st1st  11425  swrd00g  11437  swrdlend  11446  swrds1  11456  cats1lend  11555  cats2catd  11557  s2leng  11577  s2dmg  11578  imre  11632  reim0b  11643  rereb  11644  sq01  11676  resqrexlemover  11792  resqrexlemcalc1  11796  abs00bd  11848  maxabslemlub  11990  xrmaxiflemcom  12034  xrmaxadd  12046  climconst  12075  fzf1o  12161  isumz  12175  fsumf1o  12176  fsumcllem  12185  fsumadd  12192  fsumxp  12222  fsumcnv  12223  fsummulc2  12234  fsumconst  12240  fsumabs  12251  telfsumo  12252  fsumparts  12256  fsumrelem  12257  fsumiun  12263  binomlem  12269  binom  12270  binom11  12272  isumsplit  12277  arisum  12284  arisum2  12285  trireciplem  12286  georeclim  12299  cvgratnnlemseq  12312  prodfrecap  12332  prod1dc  12372  fprodf1o  12374  fprodcl2lem  12391  fprodcllem  12392  fprodfac  12401  fprod2d  12409  fprodxp  12410  fprodcnv  12411  fprodrec  12415  fprodmodd  12427  ef0lem  12446  ege2le3  12457  efaddlem  12460  efcan  12462  eft0val  12479  ef4p  12480  efgt1p2  12481  efi4p  12503  sincossq  12534  cos2tsin  12537  absefi  12555  demoivreALT  12560  p1modz1  12580  dvdsabseq  12633  odd2np1lem  12658  oddp1even  12662  opoe  12681  m1expo  12686  m1exp1  12687  nn0o1gt2  12691  bitsinv1  12748  gcddvds  12759  gcdcl  12762  gcdeq0  12773  gcd0id  12775  bezoutr1  12829  nnmindc  12830  nnminle  12831  eucalg  12856  lcm0val  12862  lcmid  12877  rpmul  12895  dfphi2  13021  phiprmpw  13023  hashgcdeq  13041  odzdvds  13047  nnnn0modprm0  13057  pythagtriplem4  13070  pythagtriplem12  13077  pcaddlem  13141  pcmpt  13145  pockthi  13160  4sqlem12  13204  2expltfac  13242  prmlem0  13243  ballotfilemfp1  13283  ballotfilemfval0  13287  ballotfilemsv  13305  ennnfonelem0  13348  ennnfonelem1  13350  ennnfonelemhdmp1  13352  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemf1  13361  ctiunctlemfo  13382  setsresg  13442  strressid  13478  strle1g  13513  restid2  13655  gzsumwmhm  13856  grplactcnv  13960  mulg0  13981  mulgnn0gzsum  13984  mulgneg  13996  mulgneg2  14012  gzsumconst  14227  gzsumsnfd  14231  gzsumsplit0  14232  gsumvalfi  14236  gsumsncmn  14240  gsump1  14241  gsummptfidmadd  14245  gsummptfidmsplit  14248  gsumresfi  14254  gsummhmfi  14255  prdsbas3  14278  zrhval2  15045  assamulgscmlem2  15133  mpl0fi  15192  tgval2  15251  tgidm  15274  epttop  15290  tgrest  15369  restco  15374  restsn  15380  tgcn  15408  cnptopresti  15438  cnptoprest  15439  txbas  15458  upxp  15472  txrest  15476  txdis  15477  txhmeo  15519  txswaphmeolem  15520  xblss2ps  15604  xblss2  15605  qtopbasss  15721  fsumcncntop  15767  hoverb  15848  limcimolemlt  15864  dvcnp2cntop  15899  dvcoapbr  15907  dvexp  15911  dvexp2  15912  dvmptid  15916  dveflem  15926  dvef  15927  plymullem1  15948  plyadd  15951  plymul  15952  plycoeid3  15957  plycjlemc  15960  plycj  15961  sin0pilem1  15982  sin2kpi  16012  cos2kpi  16013  coseq0q4123  16035  coseq0negpitopi  16037  sincosq1eq  16040  sinkpi  16048  coskpi  16049  sineq0re  16050  root1idef  16058  logfac  16100  1cxp  16107  birthdaylem2  16200  birthdaylem3  16201  efnnfsumcl  16213  ppiprm  16233  chtprm  16235  chtdif  16238  efchtqdvds  16239  ppidif  16243  ppiqltx  16255  prmorcht  16256  mpodvdsmulf1o  16258  chtublem  16269  chtqub  16270  bclbnd  16281  bposlem1  16285  bposlem2  16286  bposlem5  16289  bposlem6  16290  bposlem8  16292  bposlem9  16293  lgslem2  16299  lgsfcl2  16304  lgs0  16311  lgs2  16315  lgsneg  16322  lgsdilem  16325  lgsdir2lem4  16329  lgsdir2lem5  16330  lgsne0  16336  lgssq  16338  lgssq2  16339  gausslemma2dlem3  16361  gausslemma2dlem4  16362  lgseisenlem1  16368  lgsquadlem2  16376  lgsquad2lem2  16380  lgsquad3  16382  m1lgs  16383  2lgslem1a2  16385  2lgsoddprmlem3  16409  2sqlem9  16422  2sqlem10  16423  edgiedgbg  16485  isuhgrm  16491  isushgrm  16492  uhgr0vb  16504  uhgrun  16506  isupgren  16515  isumgren  16525  umgrnloop0  16537  upgrun  16546  umgrun  16548  isuspgren  16577  isusgren  16578  usgrf1oedg  16625  usgredg3  16634  egrsubgr  16683  0uhgrsubgr  16685  uhgrspansubgrlem  16696  vtxdg0v  16714  vtxdgfi0e  16715  vtxdfifiun  16717  vtxdumgrfival  16718  1loopgrvd2fi  16725  vdegp1cid  16736  wlkl1loop  16778  2wlklem  16796  upgr2wlkdc  16797  clwwlkn0  16828  clwwlkn1  16838  clwwlkn2  16841  umgr2cwwk2dif  16844  clwwlk0on0  16851  clwwlknonel  16852  clwwlknonex2lem1  16857  trlsegvdeglem4  16883  eupthvdres  16895  eupth2lembfi  16897  konigsberglem1  16908  konigsberglem2  16909  konigsberglem3  16910  ex-ceil  16919  bj-intexr  17113  wexmiddiffilem  17222  wexmiddifxylem  17224  peano3nninf  17229  nninfall  17231  isomninnlem  17258  iswomni0  17281  ismkvnnlem  17282  nconstwlpolem0  17293