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  gsummhmfi  14248  prdsbas3  14271  zrhval2  15038  assamulgscmlem2  15126  mpl0fi  15184  tgval2  15243  tgidm  15266  epttop  15282  tgrest  15361  restco  15366  restsn  15372  tgcn  15400  cnptopresti  15430  cnptoprest  15431  txbas  15450  upxp  15464  txrest  15468  txdis  15469  txhmeo  15511  txswaphmeolem  15512  xblss2ps  15596  xblss2  15597  qtopbasss  15713  fsumcncntop  15759  hoverb  15840  limcimolemlt  15856  dvcnp2cntop  15891  dvcoapbr  15899  dvexp  15903  dvexp2  15904  dvmptid  15908  dveflem  15918  dvef  15919  plymullem1  15940  plyadd  15943  plymul  15944  plycoeid3  15949  plycjlemc  15952  plycj  15953  sin0pilem1  15974  sin2kpi  16004  cos2kpi  16005  coseq0q4123  16027  coseq0negpitopi  16029  sincosq1eq  16032  sinkpi  16040  coskpi  16041  logfac  16090  1cxp  16097  birthdaylem2  16187  birthdaylem3  16188  efnnfsumcl  16200  ppiprm  16220  chtprm  16222  chtdif  16225  efchtqdvds  16226  ppidif  16230  ppiqltx  16242  prmorcht  16243  mpodvdsmulf1o  16245  chtublem  16256  chtqub  16257  bclbnd  16268  bposlem1  16272  bposlem2  16273  bposlem5  16276  bposlem6  16277  bposlem8  16279  bposlem9  16280  lgslem2  16286  lgsfcl2  16291  lgs0  16298  lgs2  16302  lgsneg  16309  lgsdilem  16312  lgsdir2lem4  16316  lgsdir2lem5  16317  lgsne0  16323  lgssq  16325  lgssq2  16326  gausslemma2dlem3  16348  gausslemma2dlem4  16349  lgseisenlem1  16355  lgsquadlem2  16363  lgsquad2lem2  16367  lgsquad3  16369  m1lgs  16370  2lgslem1a2  16372  2lgsoddprmlem3  16396  2sqlem9  16409  2sqlem10  16410  edgiedgbg  16472  isuhgrm  16478  isushgrm  16479  uhgr0vb  16491  uhgrun  16493  isupgren  16502  isumgren  16512  umgrnloop0  16524  upgrun  16533  umgrun  16535  isuspgren  16564  isusgren  16565  usgrf1oedg  16612  usgredg3  16621  egrsubgr  16670  0uhgrsubgr  16672  uhgrspansubgrlem  16683  vtxdg0v  16701  vtxdgfi0e  16702  vtxdfifiun  16704  vtxdumgrfival  16705  1loopgrvd2fi  16712  vdegp1cid  16723  wlkl1loop  16765  2wlklem  16783  upgr2wlkdc  16784  clwwlkn0  16815  clwwlkn1  16825  clwwlkn2  16828  umgr2cwwk2dif  16831  clwwlk0on0  16838  clwwlknonel  16839  clwwlknonex2lem1  16844  trlsegvdeglem4  16870  eupthvdres  16882  eupth2lembfi  16884  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  ex-ceil  16906  bj-intexr  17100  wexmiddiffilem  17209  wexmiddifxylem  17211  peano3nninf  17216  nninfall  17218  isomninnlem  17245  iswomni0  17268  ismkvnnlem  17269  nconstwlpolem0  17280