Theorem eqtrdi 2283

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 2267	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 2216

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

This theorem is referenced by:  eqtr2di  2284  eqtr4di  2285  3eqtr3g  2290  3eqtr4a  2293  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  csbprc  3558  un00  3559  disjssun  3576  disjpr2  3758  tppreq3  3799  diftpsn3  3840  ssprsseq  3861  preq12b  3879  intsng  3988  uniintsnr  3990  rint0  3993  riin0  4068  iununir  4080  intexr  4267  exmid1stab  4326  sucprc  4538  op1stbg  4605  elreldm  4988  xpeq0r  5190  xpdisj1  5192  xpdisj2  5193  resdisj  5196  xpima1  5214  xpima2m  5215  elxp4  5255  unixp0im  5304  uniabio  5328  iotass  5335  cnvresid  5435  funimacnv  5437  fresaunres2disj  5550  fimadmfo  5604  f1o00  5656  dffv4g  5672  fv2prc  5714  fnrnfv  5728  feqresmpt  5736  dffn5imf  5737  funfvdm2f  5747  fvun1  5748  fvmpt2  5766  fndmin  5790  fmptcof  5849  fmptcos  5850  funopdmsn  5869  fvunsng  5883  fvpr1  5893  dfimafnf  5928  fnrnov  6208  f1o3d  6271  offval  6283  ofrfval  6284  op1std  6355  op2ndd  6356  fmpoco  6425  suppsnopdc  6463  mptsuppdifd  6468  supp0cosupp0fn  6480  tpostpos  6508  tfr0  6567  rdgival  6626  frec0g  6641  2oconcl  6685  om0  6704  oei0  6705  oasuc  6710  omv2  6711  nnm0r  6725  uniqs2  6842  en1  7052  en1bg  7053  fundmen  7060  mapsnen  7066  en2  7078  xpsnen  7085  xpcomco  7090  xpdom2  7095  xpmapenlem  7115  exmidpweq  7182  unsnfidcex  7193  fiintim  7204  ssfirab  7210  sbthlemi8  7247  elfi2  7272  fi0  7275  fieq0  7276  djudom  7397  ismkvnex  7459  nninfwlpoimlemg  7479  en2other2  7512  exmidfodomrlemim  7517  nq0m0r  7787  addpinq1  7795  genipv  7840  genpelvl  7843  genpelvu  7844  cauappcvgprlem1  7990  caucvgsrlemoffres  8131  addresr  8168  mulresr  8169  axcnre  8212  add20  8765  rimul  8876  rereim  8877  mulreim  8895  sup3exmid  9248  fv0p1e1  9369  div4p1lem1div2  9509  nnm1nn0  9554  znegcl  9625  peano2z  9630  nneoor  9698  nn0ind-raph  9713  xnegneg  10185  xltnegi  10187  xaddpnf1  10198  xnegid  10211  xnn0xadd0  10219  xnegdi  10220  xsubge0  10233  xposdif  10234  xlesubadd  10235  xleaddadd  10239  fz0to4untppr  10480  fzo0to2pr  10585  nninfdcex  10621  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  mulp1mod1  10751  frecfzennn  10812  iseqf1olemqk  10893  exp0  10929  expp1  10932  expnegap0  10933  1exp  10954  mulexp  10964  m1expeven  10972  sq0i  11017  bernneq  11047  facp1  11117  faclbnd3  11130  facubnd  11132  bcval5  11150  hashinfom  11166  hashsng  11186  hashxp  11216  hashpwfi  11218  resunimafz0  11223  ssenneg  11229  hashfibclem  11231  hashfibc  11232  zfz1iso  11238  hash2en  11240  hashtpgim  11242  lsw1  11299  s1rn  11331  eqs1  11341  ccat1st1st  11354  swrd00g  11366  swrdlend  11375  swrds1  11385  cats1lend  11484  cats2catd  11486  s2leng  11506  s2dmg  11507  imre  11561  reim0b  11572  rereb  11573  resqrexlemover  11720  resqrexlemcalc1  11724  abs00bd  11776  maxabslemlub  11917  xrmaxiflemcom  11959  xrmaxadd  11971  climconst  12000  fzf1o  12086  isumz  12100  fsumf1o  12101  fsumcllem  12110  fsumadd  12117  fsumxp  12147  fsumcnv  12148  fsummulc2  12159  fsumconst  12165  fsumabs  12176  telfsumo  12177  fsumparts  12181  fsumrelem  12182  fsumiun  12188  binomlem  12194  binom  12195  binom11  12197  isumsplit  12202  arisum  12209  arisum2  12210  trireciplem  12211  georeclim  12224  cvgratnnlemseq  12237  prodfrecap  12257  prod1dc  12297  fprodf1o  12299  fprodcl2lem  12316  fprodcllem  12317  fprodfac  12326  fprod2d  12334  fprodxp  12335  fprodcnv  12336  fprodrec  12340  fprodmodd  12352  ef0lem  12371  ege2le3  12382  efaddlem  12385  efcan  12387  eft0val  12404  ef4p  12405  efgt1p2  12406  efi4p  12428  sincossq  12459  cos2tsin  12462  absefi  12480  demoivreALT  12485  p1modz1  12505  dvdsabseq  12558  odd2np1lem  12583  oddp1even  12587  opoe  12606  m1expo  12611  m1exp1  12612  nn0o1gt2  12616  bitsinv1  12673  gcddvds  12684  gcdcl  12687  gcdeq0  12698  gcd0id  12700  bezoutr1  12754  nnmindc  12755  nnminle  12756  eucalg  12781  lcm0val  12787  lcmid  12802  rpmul  12820  dfphi2  12942  phiprmpw  12944  hashgcdeq  12962  odzdvds  12968  nnnn0modprm0  12978  pythagtriplem4  12991  pythagtriplem12  12998  pcaddlem  13062  pcmpt  13066  pockthi  13081  4sqlem12  13125  2expltfac  13162  ballotfilemfp1  13175  ballotfilemfval0  13179  ballotfilemsv  13197  ennnfonelem0  13240  ennnfonelem1  13242  ennnfonelemhdmp1  13244  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemf1  13253  ctiunctlemfo  13274  setsresg  13334  strressid  13368  strle1g  13403  restid2  13545  gsumwmhm  13753  grplactcnv  13857  mulg0  13878  mulgnn0gsum  13881  mulgneg  13893  mulgneg2  13909  gsumfzconst  14094  gsumfzsnfd  14098  gsumsplit0  14099  gfsumval  14102  gfsumsn  14107  gfsump1  14108  prdsbas3  14129  gsumfzfsumlem0  14860  zrhval2  14893  mpl0fi  14983  tgval2  15042  tgidm  15065  epttop  15081  tgrest  15160  restco  15165  restsn  15171  tgcn  15199  cnptopresti  15229  cnptoprest  15230  txbas  15249  upxp  15263  txrest  15267  txdis  15268  txhmeo  15310  txswaphmeolem  15311  xblss2ps  15395  xblss2  15396  qtopbasss  15512  fsumcncntop  15558  hoverb  15639  limcimolemlt  15655  dvcnp2cntop  15690  dvcoapbr  15698  dvexp  15702  dvexp2  15703  dvmptid  15707  dveflem  15717  dvef  15718  plymullem1  15739  plyadd  15742  plymul  15743  plycoeid3  15748  plycjlemc  15751  plycj  15752  sin0pilem1  15772  sin2kpi  15802  cos2kpi  15803  coseq0q4123  15825  coseq0negpitopi  15827  sincosq1eq  15830  sinkpi  15838  coskpi  15839  1cxp  15891  mpodvdsmulf1o  15984  lgslem2  16000  lgsfcl2  16005  lgs0  16012  lgs2  16016  lgsneg  16023  lgsdilem  16026  lgsdir2lem4  16030  lgsdir2lem5  16031  lgsne0  16037  lgssq  16039  lgssq2  16040  gausslemma2dlem3  16062  gausslemma2dlem4  16063  lgseisenlem1  16069  lgsquadlem2  16077  lgsquad2lem2  16081  lgsquad3  16083  m1lgs  16084  2lgslem1a2  16086  2lgsoddprmlem3  16110  2sqlem9  16123  2sqlem10  16124  edgiedgbg  16186  isuhgrm  16192  isushgrm  16193  uhgr0vb  16205  uhgrun  16207  isupgren  16216  isumgren  16226  umgrnloop0  16238  upgrun  16247  umgrun  16249  isuspgren  16278  isusgren  16279  usgrf1oedg  16326  usgredg3  16335  egrsubgr  16384  0uhgrsubgr  16386  uhgrspansubgrlem  16397  vtxdg0v  16415  vtxdgfi0e  16416  vtxdfifiun  16418  vtxdumgrfival  16419  1loopgrvd2fi  16426  vdegp1cid  16437  wlkl1loop  16479  2wlklem  16497  upgr2wlkdc  16498  clwwlkn0  16529  clwwlkn1  16539  clwwlkn2  16542  umgr2cwwk2dif  16545  clwwlk0on0  16552  clwwlknonel  16553  clwwlknonex2lem1  16558  trlsegvdeglem4  16584  eupthvdres  16596  eupth2lembfi  16598  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  ex-ceil  16620  bj-intexr  16804  peano3nninf  16911  nninfall  16913  isomninnlem  16940  iswomni0  16962  ismkvnnlem  16963  nconstwlpolem0  16975