Theorem eqtrdi 2278

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtr2di  2279  eqtr4di  2280  3eqtr3g  2285  3eqtr4a  2288  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  csbprc  3538  un00  3539  disjssun  3556  disjpr2  3731  tppreq3  3772  diftpsn3  3812  ssprsseq  3833  preq12b  3851  intsng  3960  uniintsnr  3962  rint0  3965  riin0  4040  iununir  4052  intexr  4238  exmid1stab  4296  sucprc  4507  op1stbg  4574  elreldm  4956  xpeq0r  5157  xpdisj1  5159  xpdisj2  5160  resdisj  5163  xpima1  5181  xpima2m  5182  elxp4  5222  unixp0im  5271  uniabio  5295  iotass  5302  cnvresid  5401  funimacnv  5403  fimadmfo  5565  f1o00  5616  dffv4g  5632  fv2prc  5674  fnrnfv  5688  feqresmpt  5696  dffn5imf  5697  funfvdm2f  5707  fvun1  5708  fvmpt2  5726  fndmin  5750  fmptcof  5810  fmptcos  5811  funopdmsn  5829  fvunsng  5843  fvpr1  5853  fnrnov  6163  offval  6238  ofrfval  6239  op1std  6306  op2ndd  6307  fmpoco  6376  tpostpos  6425  tfr0  6484  rdgival  6543  frec0g  6558  2oconcl  6602  om0  6621  oei0  6622  oasuc  6627  omv2  6628  nnm0r  6642  uniqs2  6759  en1  6968  en1bg  6969  fundmen  6976  mapsnen  6981  en2  6993  xpsnen  7000  xpcomco  7005  xpdom2  7010  xpmapenlem  7030  exmidpweq  7094  unsnfidcex  7105  fiintim  7116  ssfirab  7121  sbthlemi8  7154  elfi2  7162  fi0  7165  fieq0  7166  djudom  7283  ismkvnex  7345  nninfwlpoimlemg  7365  en2other2  7397  exmidfodomrlemim  7402  nq0m0r  7666  addpinq1  7674  genipv  7719  genpelvl  7722  genpelvu  7723  cauappcvgprlem1  7869  caucvgsrlemoffres  8010  addresr  8047  mulresr  8048  axcnre  8091  add20  8644  rimul  8755  rereim  8756  mulreim  8774  sup3exmid  9127  fv0p1e1  9248  div4p1lem1div2  9388  nnm1nn0  9433  znegcl  9500  peano2z  9505  nneoor  9572  nn0ind-raph  9587  xnegneg  10058  xltnegi  10060  xaddpnf1  10071  xnegid  10084  xnn0xadd0  10092  xnegdi  10093  xsubge0  10106  xposdif  10107  xlesubadd  10108  xleaddadd  10112  fz0to4untppr  10349  fzo0to2pr  10453  nninfdcex  10487  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  mulp1mod1  10617  frecfzennn  10678  iseqf1olemqk  10759  exp0  10795  expp1  10798  expnegap0  10799  1exp  10820  mulexp  10830  m1expeven  10838  sq0i  10883  bernneq  10912  facp1  10982  faclbnd3  10995  facubnd  10997  bcval5  11015  hashinfom  11030  hashsng  11050  hashxp  11080  resunimafz0  11085  zfz1iso  11095  hash2en  11097  lsw1  11153  s1rn  11185  eqs1  11195  ccat1st1st  11208  swrd00g  11220  swrdlend  11229  swrds1  11239  cats1lend  11338  cats2catd  11340  s2leng  11360  s2dmg  11361  imre  11402  reim0b  11413  rereb  11414  resqrexlemover  11561  resqrexlemcalc1  11565  abs00bd  11617  maxabslemlub  11758  xrmaxiflemcom  11800  xrmaxadd  11812  climconst  11841  isumz  11940  fsumf1o  11941  fsumcllem  11950  fsumadd  11957  fsumxp  11987  fsumcnv  11988  fsummulc2  11999  fsumconst  12005  fsumabs  12016  telfsumo  12017  fsumparts  12021  fsumrelem  12022  fsumiun  12028  binomlem  12034  binom  12035  binom11  12037  isumsplit  12042  arisum  12049  arisum2  12050  trireciplem  12051  georeclim  12064  cvgratnnlemseq  12077  prodfrecap  12097  prod1dc  12137  fprodf1o  12139  fprodcl2lem  12156  fprodcllem  12157  fprodfac  12166  fprod2d  12174  fprodxp  12175  fprodcnv  12176  fprodrec  12180  fprodmodd  12192  ef0lem  12211  ege2le3  12222  efaddlem  12225  efcan  12227  eft0val  12244  ef4p  12245  efgt1p2  12246  efi4p  12268  sincossq  12299  cos2tsin  12302  absefi  12320  demoivreALT  12325  p1modz1  12345  dvdsabseq  12398  odd2np1lem  12423  oddp1even  12427  opoe  12446  m1expo  12451  m1exp1  12452  nn0o1gt2  12456  bitsinv1  12513  gcddvds  12524  gcdcl  12527  gcdeq0  12538  gcd0id  12540  bezoutr1  12594  nnmindc  12595  nnminle  12596  eucalg  12621  lcm0val  12627  lcmid  12642  rpmul  12660  dfphi2  12782  phiprmpw  12784  hashgcdeq  12802  odzdvds  12808  nnnn0modprm0  12818  pythagtriplem4  12831  pythagtriplem12  12838  pcaddlem  12902  pcmpt  12906  pockthi  12921  4sqlem12  12965  2expltfac  13002  ennnfonelem0  13016  ennnfonelem1  13018  ennnfonelemhdmp1  13020  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemf1  13029  ctiunctlemfo  13050  setsresg  13110  strressid  13144  strle1g  13179  restid2  13321  prdsbas3  13360  gsumwmhm  13571  grplactcnv  13675  mulg0  13702  mulgnn0gsum  13705  mulgneg  13717  mulgneg2  13733  gsumfzconst  13918  gsumfzsnfd  13922  gsumfzfsumlem0  14590  zrhval2  14623  mpl0fi  14706  tgval2  14765  tgidm  14788  epttop  14804  tgrest  14883  restco  14888  restsn  14894  tgcn  14922  cnptopresti  14952  cnptoprest  14953  txbas  14972  upxp  14986  txrest  14990  txdis  14991  txhmeo  15033  txswaphmeolem  15034  xblss2ps  15118  xblss2  15119  qtopbasss  15235  fsumcncntop  15281  hoverb  15362  limcimolemlt  15378  dvcnp2cntop  15413  dvcoapbr  15421  dvexp  15425  dvexp2  15426  dvmptid  15430  dveflem  15440  dvef  15441  plymullem1  15462  plyadd  15465  plymul  15466  plycoeid3  15471  plycjlemc  15474  plycj  15475  sin0pilem1  15495  sin2kpi  15525  cos2kpi  15526  coseq0q4123  15548  coseq0negpitopi  15550  sincosq1eq  15553  sinkpi  15561  coskpi  15562  1cxp  15614  mpodvdsmulf1o  15704  lgslem2  15720  lgsfcl2  15725  lgs0  15732  lgs2  15736  lgsneg  15743  lgsdilem  15746  lgsdir2lem4  15750  lgsdir2lem5  15751  lgsne0  15757  lgssq  15759  lgssq2  15760  gausslemma2dlem3  15782  gausslemma2dlem4  15783  lgseisenlem1  15789  lgsquadlem2  15797  lgsquad2lem2  15801  lgsquad3  15803  m1lgs  15804  2lgslem1a2  15806  2lgsoddprmlem3  15830  2sqlem9  15843  2sqlem10  15844  edgiedgbg  15906  isuhgrm  15912  isushgrm  15913  uhgr0vb  15925  uhgrun  15927  isupgren  15936  isumgren  15946  umgrnloop0  15958  upgrun  15965  umgrun  15967  isuspgren  15996  isusgren  15997  usgrf1oedg  16044  usgredg3  16053  vtxdg0v  16100  vtxdgfi0e  16101  vtxdfifiun  16103  vtxdumgrfival  16104  1loopgrvd2fi  16111  wlkl1loop  16155  2wlklem  16171  upgr2wlkdc  16172  clwwlkn0  16203  clwwlkn1  16213  clwwlkn2  16216  umgr2cwwk2dif  16219  clwwlk0on0  16226  clwwlknonel  16227  clwwlknonex2lem1  16232  ex-ceil  16258  bj-intexr  16439  peano3nninf  16545  nninfall  16547  isomninnlem  16570  iswomni0  16591  ismkvnnlem  16592  nconstwlpolem0  16603