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  6540  tfr0  6599  rdgival  6658  frec0g  6673  2oconcl  6717  om0  6736  oei0  6737  oasuc  6742  omv2  6743  nnm0r  6757  uniqs2  6874  en1  7092  en1bg  7093  fundmen  7100  mapsnen  7106  en2  7118  xpsnen  7125  xpcomco  7130  xpdom2  7135  xpmapenlem  7155  exmidpweq  7222  unsnfidcex  7233  fiintim  7244  ssfirab  7250  sbthlemi8  7288  snopfsupp  7306  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  9684  peano2z  9689  nneoor  9758  nn0ind-raph  9773  xnegneg  10251  xltnegi  10253  xaddpnf1  10264  xnegid  10277  xnn0xadd0  10285  xnegdi  10286  xsubge0  10299  xposdif  10300  xlesubadd  10301  xleaddadd  10305  fz0to4untppr  10547  fzo0to2pr  10652  nninfdcex  10688  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  mulp1mod1  10822  frecfzennn  10883  iseqf1olemqk  10964  exp0  11000  expp1  11003  expnegap0  11004  1exp  11025  mulexp  11035  m1expeven  11043  sq0i  11088  bernneq  11118  facp1  11189  faclbnd3  11202  facubnd  11204  bcval5  11222  hashinfom  11238  hashsng  11258  hashxp  11288  hashpwfi  11290  resunimafz0  11295  ssenneg  11301  hashfibclem  11303  hashfibc  11304  hashf1lem2  11307  hashf1  11308  zfz1iso  11314  hash2en  11316  hashtpgim  11318  lsw1  11375  s1rn  11407  eqs1  11417  ccat1st1st  11430  swrd00g  11442  swrdlend  11451  swrds1  11461  cats1lend  11560  cats2catd  11562  s2leng  11582  s2dmg  11583  imre  11637  reim0b  11648  rereb  11649  sq01  11681  resqrexlemover  11797  resqrexlemcalc1  11801  abs00bd  11853  maxabslemlub  11995  xrmaxiflemcom  12039  xrmaxadd  12051  climconst  12080  fzf1o  12166  isumz  12180  fsumf1o  12181  fsumcllem  12190  fsumadd  12197  fsumxp  12227  fsumcnv  12228  fsummulc2  12239  fsumconst  12245  fsumabs  12256  telfsumo  12257  fsumparts  12261  fsumrelem  12262  fsumiun  12268  binomlem  12274  binom  12275  binom11  12277  isumsplit  12282  arisum  12289  arisum2  12290  trireciplem  12291  georeclim  12304  cvgratnnlemseq  12317  prodfrecap  12337  prod1dc  12377  fprodf1o  12379  fprodcl2lem  12396  fprodcllem  12397  fprodfac  12406  fprod2d  12414  fprodxp  12415  fprodcnv  12416  fprodrec  12420  fprodmodd  12432  ef0lem  12451  ege2le3  12462  efaddlem  12465  efcan  12467  eft0val  12484  ef4p  12485  efgt1p2  12486  efi4p  12508  sincossq  12539  cos2tsin  12542  absefi  12560  demoivreALT  12565  p1modz1  12585  dvdsabseq  12638  odd2np1lem  12663  oddp1even  12667  opoe  12686  m1expo  12691  m1exp1  12692  nn0o1gt2  12696  bitsinv1  12753  gcddvds  12764  gcdcl  12767  gcdeq0  12778  gcd0id  12780  bezoutr1  12834  nnmindc  12835  nnminle  12836  eucalg  12861  lcm0val  12867  lcmid  12882  rpmul  12900  dfphi2  13026  phiprmpw  13028  hashgcdeq  13046  odzdvds  13052  nnnn0modprm0  13062  pythagtriplem4  13075  pythagtriplem12  13082  pcaddlem  13146  pcmpt  13150  pockthi  13165  4sqlem12  13209  2expltfac  13247  prmlem0  13248  ballotfilemfp1  13288  ballotfilemfval0  13292  ballotfilemsv  13310  ennnfonelem0  13353  ennnfonelem1  13355  ennnfonelemhdmp1  13357  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemf1  13366  ctiunctlemfo  13387  setsresg  13447  strressid  13483  strle1g  13518  restid2  13660  gzsumwmhm  13861  grplactcnv  13965  mulg0  13986  mulgnn0gzsum  13989  mulgneg  14001  mulgneg2  14017  gzsumconst  14232  gzsumsnfd  14236  gzsumsplit0  14237  gsumvalfi  14241  gsumsncmn  14245  gsump1  14246  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsumresfi  14262  gsummhmfi  14263  gsum2dfilem2  14271  gsum2dfi  14272  gsum2d2fi  14273  gsumcom2fi  14274  prdsbas3  14293  zrhval2  15062  assamulgscmlem2  15150  mvridfi  15217  mpl0fi  15235  tgval2  15294  tgidm  15317  epttop  15333  tgrest  15412  restco  15417  restsn  15423  tgcn  15451  cnptopresti  15481  cnptoprest  15482  txbas  15501  upxp  15515  txrest  15519  txdis  15520  txhmeo  15562  txswaphmeolem  15563  xblss2ps  15647  xblss2  15648  qtopbasss  15764  fsumcncntop  15810  hoverb  15891  limcimolemlt  15907  dvcnp2cntop  15942  dvcoapbr  15950  dvexp  15954  dvexp2  15955  dvmptid  15959  dveflem  15969  dvef  15970  plymullem1  15991  plyadd  15994  plymul  15995  plycoeid3  16000  plycjlemc  16003  plycj  16004  sin0pilem1  16025  sin2kpi  16055  cos2kpi  16056  coseq0q4123  16078  coseq0negpitopi  16080  sincosq1eq  16083  sinkpi  16091  coskpi  16092  sineq0re  16093  root1idef  16101  logfac  16143  1cxp  16150  birthdaylem2  16243  birthdaylem3  16244  efnnfsumcl  16256  ppiprm  16276  chtprm  16278  chtdif  16281  efchtqdvds  16282  ppidif  16286  ppiqltx  16298  prmorcht  16299  mpodvdsmulf1o  16301  chtublem  16312  chtqub  16313  bclbnd  16324  bposlem1  16328  bposlem2  16329  bposlem5  16332  bposlem6  16333  bposlem8  16335  bposlem9  16336  lgslem2  16342  lgsfcl2  16347  lgs0  16354  lgs2  16358  lgsneg  16365  lgsdilem  16368  lgsdir2lem4  16372  lgsdir2lem5  16373  lgsne0  16379  lgssq  16381  lgssq2  16382  gausslemma2dlem3  16404  gausslemma2dlem4  16405  lgseisenlem1  16411  lgsquadlem2  16419  lgsquad2lem2  16423  lgsquad3  16425  m1lgs  16426  2lgslem1a2  16428  2lgsoddprmlem3  16452  2sqlem9  16465  2sqlem10  16466  edgiedgbg  16528  isuhgrm  16534  isushgrm  16535  uhgr0vb  16547  uhgrun  16549  isupgren  16558  isumgren  16568  umgrnloop0  16580  upgrun  16589  umgrun  16591  isuspgren  16620  isusgren  16621  usgrf1oedg  16668  usgredg3  16677  egrsubgr  16726  0uhgrsubgr  16728  uhgrspansubgrlem  16739  vtxdg0v  16757  vtxdgfi0e  16758  vtxdfifiun  16760  vtxdumgrfival  16761  1loopgrvd2fi  16768  vdegp1cid  16779  wlkl1loop  16821  2wlklem  16839  upgr2wlkdc  16840  clwwlkn0  16871  clwwlkn1  16881  clwwlkn2  16884  umgr2cwwk2dif  16887  clwwlk0on0  16894  clwwlknonel  16895  clwwlknonex2lem1  16900  trlsegvdeglem4  16926  eupthvdres  16938  eupth2lembfi  16940  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  ex-ceil  16962  bj-intexr  17156  wexmiddiffilem  17265  wexmiddifxylem  17267  peano3nninf  17273  nninfall  17275  isomninnlem  17302  iswomni0  17325  ismkvnnlem  17326  nconstwlpolem0  17337