Theorem eqtrdi 2215

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

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  eqtr2di  2216  eqtr4di  2217  3eqtr3g  2222  3eqtr4a  2225  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  csbprc  3454  un00  3455  disjssun  3472  disjpr2  3640  tppreq3  3679  diftpsn3  3714  preq12b  3750  intsng  3858  uniintsnr  3860  rint0  3863  riin0  3937  iununir  3949  intexr  4129  sucprc  4390  op1stbg  4457  elreldm  4830  xpeq0r  5026  xpdisj1  5028  xpdisj2  5029  resdisj  5032  xpima1  5050  xpima2m  5051  elxp4  5091  unixp0im  5140  uniabio  5163  iotass  5170  cnvresid  5262  funimacnv  5264  f1o00  5467  dffv4g  5483  fnrnfv  5533  feqresmpt  5540  dffn5imf  5541  funfvdm2f  5551  fvun1  5552  fvmpt2  5569  fndmin  5592  fmptcof  5652  fmptcos  5653  fvunsng  5679  fvpr1  5689  fnrnov  5987  offval  6057  ofrfval  6058  op1std  6116  op2ndd  6117  fmpoco  6184  tpostpos  6232  tfr0  6291  rdgival  6350  frec0g  6365  2oconcl  6407  om0  6426  oei0  6427  oasuc  6432  omv2  6433  nnm0r  6447  uniqs2  6561  en1  6765  en1bg  6766  fundmen  6772  mapsnen  6777  xpsnen  6787  xpcomco  6792  xpdom2  6797  xpmapenlem  6815  exmidpweq  6875  unsnfidcex  6885  fiintim  6894  ssfirab  6899  sbthlemi8  6929  elfi2  6937  fi0  6940  fieq0  6941  djudom  7058  ismkvnex  7119  en2other2  7152  exmidfodomrlemim  7157  nq0m0r  7397  addpinq1  7405  genipv  7450  genpelvl  7453  genpelvu  7454  cauappcvgprlem1  7600  caucvgsrlemoffres  7741  addresr  7778  mulresr  7779  axcnre  7822  add20  8372  rimul  8483  rereim  8484  mulreim  8502  sup3exmid  8852  fv0p1e1  8972  div4p1lem1div2  9110  nnm1nn0  9155  znegcl  9222  peano2z  9227  nneoor  9293  nn0ind-raph  9308  xnegneg  9769  xltnegi  9771  xaddpnf1  9782  xnegid  9795  xnn0xadd0  9803  xnegdi  9804  xsubge0  9817  xposdif  9818  xlesubadd  9819  xleaddadd  9823  fz0to4untppr  10059  fzo0to2pr  10153  fldiv4p1lem1div2  10240  mulp1mod1  10300  frecfzennn  10361  iseqf1olemqk  10429  exp0  10459  expp1  10462  expnegap0  10463  1exp  10484  mulexp  10494  m1expeven  10502  sq0i  10546  bernneq  10575  facp1  10643  faclbnd3  10656  facubnd  10658  bcval5  10676  hashinfom  10691  hashsng  10711  hashxp  10739  resunimafz0  10744  zfz1iso  10754  imre  10793  reim0b  10804  rereb  10805  resqrexlemover  10952  resqrexlemcalc1  10956  abs00bd  11008  maxabslemlub  11149  xrmaxiflemcom  11190  xrmaxadd  11202  climconst  11231  isumz  11330  fsumf1o  11331  fsumcllem  11340  fsumadd  11347  fsumxp  11377  fsumcnv  11378  fsummulc2  11389  fsumconst  11395  fsumabs  11406  telfsumo  11407  fsumparts  11411  fsumrelem  11412  fsumiun  11418  binomlem  11424  binom  11425  binom11  11427  isumsplit  11432  arisum  11439  arisum2  11440  trireciplem  11441  georeclim  11454  cvgratnnlemseq  11467  prodfrecap  11487  prod1dc  11527  fprodf1o  11529  fprodcl2lem  11546  fprodcllem  11547  fprodfac  11556  fprod2d  11564  fprodxp  11565  fprodcnv  11566  fprodrec  11570  fprodmodd  11582  ef0lem  11601  ege2le3  11612  efaddlem  11615  efcan  11617  eft0val  11634  ef4p  11635  efgt1p2  11636  efi4p  11658  sincossq  11689  cos2tsin  11692  absefi  11709  demoivreALT  11714  p1modz1  11734  dvdsabseq  11785  odd2np1lem  11809  oddp1even  11813  opoe  11832  m1expo  11837  m1exp1  11838  nn0o1gt2  11842  nninfdcex  11886  gcddvds  11896  gcdcl  11899  gcdeq0  11910  gcd0id  11912  bezoutr1  11966  nnmindc  11967  nnminle  11968  eucalg  11991  lcm0val  11997  lcmid  12012  rpmul  12030  dfphi2  12152  phiprmpw  12154  hashgcdeq  12171  odzdvds  12177  nnnn0modprm0  12187  pythagtriplem4  12200  pythagtriplem12  12207  pcaddlem  12270  pcmpt  12273  pockthi  12288  ennnfonelem0  12338  ennnfonelem1  12340  ennnfonelemhdmp1  12342  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemf1  12351  ctiunctlemfo  12372  setsresg  12432  strle1g  12485  restid2  12565  tgval2  12691  tgidm  12714  epttop  12730  tgrest  12809  restco  12814  restsn  12820  tgcn  12848  cnptopresti  12878  cnptoprest  12879  txbas  12898  upxp  12912  txrest  12916  txdis  12917  txhmeo  12959  txswaphmeolem  12960  xblss2ps  13044  xblss2  13045  qtopbasss  13161  fsumcncntop  13196  limcimolemlt  13273  dvcnp2cntop  13303  dvcoapbr  13311  dvexp  13315  dvexp2  13316  dveflem  13327  dvef  13328  sin0pilem1  13342  sin2kpi  13372  cos2kpi  13373  coseq0q4123  13395  coseq0negpitopi  13397  sincosq1eq  13400  sinkpi  13408  coskpi  13409  1cxp  13461  lgslem2  13542  lgsfcl2  13547  lgs0  13554  lgs2  13558  lgsneg  13565  lgsdilem  13568  lgsdir2lem4  13572  lgsdir2lem5  13573  lgsne0  13579  lgssq  13581  lgssq2  13582  2sqlem9  13600  2sqlem10  13601  ex-ceil  13607  bj-intexr  13790  exmid1stab  13880  peano3nninf  13887  nninfall  13889  isomninnlem  13909  iswomni0  13930  ismkvnnlem  13931  nconstwlpolem0  13941