Theorem eqtrdi 2281

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225

This theorem is referenced by:  eqtr2di  2282  eqtr4di  2283  3eqtr3g  2288  3eqtr4a  2291  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  csbprc  3554  un00  3555  disjssun  3572  disjpr2  3753  tppreq3  3794  diftpsn3  3835  ssprsseq  3856  preq12b  3874  intsng  3983  uniintsnr  3985  rint0  3988  riin0  4063  iununir  4075  intexr  4262  exmid1stab  4321  sucprc  4533  op1stbg  4600  elreldm  4983  xpeq0r  5185  xpdisj1  5187  xpdisj2  5188  resdisj  5191  xpima1  5209  xpima2m  5210  elxp4  5250  unixp0im  5299  uniabio  5323  iotass  5330  cnvresid  5430  funimacnv  5432  fresaunres2disj  5545  fimadmfo  5599  f1o00  5651  dffv4g  5667  fv2prc  5709  fnrnfv  5723  feqresmpt  5731  dffn5imf  5732  funfvdm2f  5742  fvun1  5743  fvmpt2  5761  fndmin  5785  fmptcof  5844  fmptcos  5845  funopdmsn  5864  fvunsng  5878  fvpr1  5888  fnrnov  6200  offval  6274  ofrfval  6275  op1std  6342  op2ndd  6343  fmpoco  6412  suppsnopdc  6450  mptsuppdifd  6455  supp0cosupp0fn  6467  tpostpos  6495  tfr0  6554  rdgival  6613  frec0g  6628  2oconcl  6672  om0  6691  oei0  6692  oasuc  6697  omv2  6698  nnm0r  6712  uniqs2  6829  en1  7039  en1bg  7040  fundmen  7047  mapsnen  7053  en2  7065  xpsnen  7072  xpcomco  7077  xpdom2  7082  xpmapenlem  7102  exmidpweq  7169  unsnfidcex  7180  fiintim  7191  ssfirab  7197  sbthlemi8  7234  elfi2  7259  fi0  7262  fieq0  7263  djudom  7384  ismkvnex  7446  nninfwlpoimlemg  7466  en2other2  7499  exmidfodomrlemim  7504  nq0m0r  7771  addpinq1  7779  genipv  7824  genpelvl  7827  genpelvu  7828  cauappcvgprlem1  7974  caucvgsrlemoffres  8115  addresr  8152  mulresr  8153  axcnre  8196  add20  8748  rimul  8859  rereim  8860  mulreim  8878  sup3exmid  9231  fv0p1e1  9352  div4p1lem1div2  9492  nnm1nn0  9537  znegcl  9608  peano2z  9613  nneoor  9680  nn0ind-raph  9695  xnegneg  10166  xltnegi  10168  xaddpnf1  10179  xnegid  10192  xnn0xadd0  10200  xnegdi  10201  xsubge0  10214  xposdif  10215  xlesubadd  10216  xleaddadd  10220  fz0to4untppr  10458  fzo0to2pr  10563  nninfdcex  10597  fldiv4p1lem1div2  10665  fldiv4lem1div2  10667  mulp1mod1  10727  frecfzennn  10788  iseqf1olemqk  10869  exp0  10905  expp1  10908  expnegap0  10909  1exp  10930  mulexp  10940  m1expeven  10948  sq0i  10993  bernneq  11022  facp1  11092  faclbnd3  11105  facubnd  11107  bcval5  11125  hashinfom  11141  hashsng  11161  hashxp  11191  hashpwfi  11193  resunimafz0  11198  ssenneg  11204  hashfibclem  11206  hashfibc  11207  zfz1iso  11213  hash2en  11215  hashtpgim  11217  lsw1  11274  s1rn  11306  eqs1  11316  ccat1st1st  11329  swrd00g  11341  swrdlend  11350  swrds1  11360  cats1lend  11459  cats2catd  11461  s2leng  11481  s2dmg  11482  imre  11536  reim0b  11547  rereb  11548  resqrexlemover  11695  resqrexlemcalc1  11699  abs00bd  11751  maxabslemlub  11892  xrmaxiflemcom  11934  xrmaxadd  11946  climconst  11975  fzf1o  12061  isumz  12075  fsumf1o  12076  fsumcllem  12085  fsumadd  12092  fsumxp  12122  fsumcnv  12123  fsummulc2  12134  fsumconst  12140  fsumabs  12151  telfsumo  12152  fsumparts  12156  fsumrelem  12157  fsumiun  12163  binomlem  12169  binom  12170  binom11  12172  isumsplit  12177  arisum  12184  arisum2  12185  trireciplem  12186  georeclim  12199  cvgratnnlemseq  12212  prodfrecap  12232  prod1dc  12272  fprodf1o  12274  fprodcl2lem  12291  fprodcllem  12292  fprodfac  12301  fprod2d  12309  fprodxp  12310  fprodcnv  12311  fprodrec  12315  fprodmodd  12327  ef0lem  12346  ege2le3  12357  efaddlem  12360  efcan  12362  eft0val  12379  ef4p  12380  efgt1p2  12381  efi4p  12403  sincossq  12434  cos2tsin  12437  absefi  12455  demoivreALT  12460  p1modz1  12480  dvdsabseq  12533  odd2np1lem  12558  oddp1even  12562  opoe  12581  m1expo  12586  m1exp1  12587  nn0o1gt2  12591  bitsinv1  12648  gcddvds  12659  gcdcl  12662  gcdeq0  12673  gcd0id  12675  bezoutr1  12729  nnmindc  12730  nnminle  12731  eucalg  12756  lcm0val  12762  lcmid  12777  rpmul  12795  dfphi2  12917  phiprmpw  12919  hashgcdeq  12937  odzdvds  12943  nnnn0modprm0  12953  pythagtriplem4  12966  pythagtriplem12  12973  pcaddlem  13037  pcmpt  13041  pockthi  13056  4sqlem12  13100  2expltfac  13137  ennnfonelem0  13156  ennnfonelem1  13158  ennnfonelemhdmp1  13160  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemf1  13169  ctiunctlemfo  13190  setsresg  13250  strressid  13284  strle1g  13319  restid2  13461  prdsbas3  13500  gsumwmhm  13711  grplactcnv  13815  mulg0  13842  mulgnn0gsum  13845  mulgneg  13857  mulgneg2  13873  gsumfzconst  14058  gsumfzsnfd  14062  gsumsplit0  14063  gsumfzfsumlem0  14734  zrhval2  14767  mpl0fi  14857  tgval2  14916  tgidm  14939  epttop  14955  tgrest  15034  restco  15039  restsn  15045  tgcn  15073  cnptopresti  15103  cnptoprest  15104  txbas  15123  upxp  15137  txrest  15141  txdis  15142  txhmeo  15184  txswaphmeolem  15185  xblss2ps  15269  xblss2  15270  qtopbasss  15386  fsumcncntop  15432  hoverb  15513  limcimolemlt  15529  dvcnp2cntop  15564  dvcoapbr  15572  dvexp  15576  dvexp2  15577  dvmptid  15581  dveflem  15591  dvef  15592  plymullem1  15613  plyadd  15616  plymul  15617  plycoeid3  15622  plycjlemc  15625  plycj  15626  sin0pilem1  15646  sin2kpi  15676  cos2kpi  15677  coseq0q4123  15699  coseq0negpitopi  15701  sincosq1eq  15704  sinkpi  15712  coskpi  15713  1cxp  15765  mpodvdsmulf1o  15858  lgslem2  15874  lgsfcl2  15879  lgs0  15886  lgs2  15890  lgsneg  15897  lgsdilem  15900  lgsdir2lem4  15904  lgsdir2lem5  15905  lgsne0  15911  lgssq  15913  lgssq2  15914  gausslemma2dlem3  15936  gausslemma2dlem4  15937  lgseisenlem1  15943  lgsquadlem2  15951  lgsquad2lem2  15955  lgsquad3  15957  m1lgs  15958  2lgslem1a2  15960  2lgsoddprmlem3  15984  2sqlem9  15997  2sqlem10  15998  edgiedgbg  16060  isuhgrm  16066  isushgrm  16067  uhgr0vb  16079  uhgrun  16081  isupgren  16090  isumgren  16100  umgrnloop0  16112  upgrun  16121  umgrun  16123  isuspgren  16152  isusgren  16153  usgrf1oedg  16200  usgredg3  16209  egrsubgr  16258  0uhgrsubgr  16260  uhgrspansubgrlem  16271  vtxdg0v  16289  vtxdgfi0e  16290  vtxdfifiun  16292  vtxdumgrfival  16293  1loopgrvd2fi  16300  vdegp1cid  16311  wlkl1loop  16353  2wlklem  16371  upgr2wlkdc  16372  clwwlkn0  16403  clwwlkn1  16413  clwwlkn2  16416  umgr2cwwk2dif  16419  clwwlk0on0  16426  clwwlknonel  16427  clwwlknonex2lem1  16432  trlsegvdeglem4  16458  eupthvdres  16470  eupth2lembfi  16472  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  ex-ceil  16494  bj-intexr  16678  peano3nninf  16785  nninfall  16787  isomninnlem  16814  iswomni0  16836  ismkvnnlem  16837  nconstwlpolem0  16849  gfsumval  16862  gfsumsn  16867  gfsump1  16868