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

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqtr2di  2288  eqtr4di  2289  3eqtr3g  2294  3eqtr4a  2297  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  un00  3566  vvin  3568  csbprc  3571  disjssun  3587  disjpr2  3769  tppreq3  3810  diftpsn3  3851  ssprsseq  3872  preq12b  3890  intsng  3999  uniintsnr  4001  rint0  4004  riin0  4079  iununir  4091  intexr  4281  exmid1stab  4340  sucprc  4552  op1stbg  4620  elreldm  5003  xpeq0r  5205  xpdisj1  5207  xpdisj2  5208  resdisj  5211  xpima1  5229  xpima2m  5230  elxp4  5270  unixp0im  5319  uniabio  5343  iotass  5350  cnvresid  5450  funimacnv  5452  fresaunres2disj  5565  fimadmfo  5619  f1o00  5671  dffv4g  5687  fv2prc  5729  fnrnfv  5743  feqresmpt  5751  dffn5imf  5752  funfvdm2f  5762  fvun1  5763  fvmpt2  5783  fndmin  5807  fmptcof  5866  fmptcos  5867  funopdmsn  5886  fvunsng  5900  fvpr1  5910  dfimafnf  5945  fnrnov  6225  f1o3d  6288  offval  6300  ofrfval  6301  op1std  6372  op2ndd  6373  fmpoco  6442  suppsnopdc  6480  mptsuppdifd  6485  supp0cosupp0fn  6497  tpostpos  6525  tfr0  6584  rdgival  6643  frec0g  6658  2oconcl  6702  om0  6721  oei0  6722  oasuc  6727  omv2  6728  nnm0r  6742  uniqs2  6859  en1  7076  en1bg  7077  fundmen  7084  mapsnen  7090  en2  7102  xpsnen  7109  xpcomco  7114  xpdom2  7119  xpmapenlem  7139  exmidpweq  7206  unsnfidcex  7217  fiintim  7228  ssfirab  7234  sbthlemi8  7271  elfi2  7296  fi0  7299  fieq0  7300  djudom  7423  ismkvnex  7485  nninfwlpoimlemg  7505  en2other2  7538  exmidfodomrlemim  7543  nq0m0r  7813  addpinq1  7821  genipv  7866  genpelvl  7869  genpelvu  7870  cauappcvgprlem1  8016  caucvgsrlemoffres  8157  addresr  8194  mulresr  8195  axcnre  8238  add20  8792  rimul  8903  rereim  8904  mulreim  8922  sup3exmid  9277  fv0p1e1  9398  div4p1lem1div2  9538  nnm1nn0  9583  znegcl  9654  peano2z  9659  nneoor  9727  nn0ind-raph  9742  xnegneg  10214  xltnegi  10216  xaddpnf1  10227  xnegid  10240  xnn0xadd0  10248  xnegdi  10249  xsubge0  10262  xposdif  10263  xlesubadd  10264  xleaddadd  10268  fz0to4untppr  10509  fzo0to2pr  10614  nninfdcex  10650  fldiv4p1lem1div2  10718  fldiv4lem1div2  10720  mulp1mod1  10780  frecfzennn  10841  iseqf1olemqk  10922  exp0  10958  expp1  10961  expnegap0  10962  1exp  10983  mulexp  10993  m1expeven  11001  sq0i  11046  bernneq  11076  facp1  11146  faclbnd3  11159  facubnd  11161  bcval5  11179  hashinfom  11195  hashsng  11215  hashxp  11245  hashpwfi  11247  resunimafz0  11252  ssenneg  11258  hashfibclem  11260  hashfibc  11261  hashf1lem2  11264  hashf1  11265  zfz1iso  11271  hash2en  11273  hashtpgim  11275  lsw1  11332  s1rn  11364  eqs1  11374  ccat1st1st  11387  swrd00g  11399  swrdlend  11408  swrds1  11418  cats1lend  11517  cats2catd  11519  s2leng  11539  s2dmg  11540  imre  11594  reim0b  11605  rereb  11606  sq01  11638  resqrexlemover  11754  resqrexlemcalc1  11758  abs00bd  11810  maxabslemlub  11951  xrmaxiflemcom  11993  xrmaxadd  12005  climconst  12034  fzf1o  12120  isumz  12134  fsumf1o  12135  fsumcllem  12144  fsumadd  12151  fsumxp  12181  fsumcnv  12182  fsummulc2  12193  fsumconst  12199  fsumabs  12210  telfsumo  12211  fsumparts  12215  fsumrelem  12216  fsumiun  12222  binomlem  12228  binom  12229  binom11  12231  isumsplit  12236  arisum  12243  arisum2  12244  trireciplem  12245  georeclim  12258  cvgratnnlemseq  12271  prodfrecap  12291  prod1dc  12331  fprodf1o  12333  fprodcl2lem  12350  fprodcllem  12351  fprodfac  12360  fprod2d  12368  fprodxp  12369  fprodcnv  12370  fprodrec  12374  fprodmodd  12386  ef0lem  12405  ege2le3  12416  efaddlem  12419  efcan  12421  eft0val  12438  ef4p  12439  efgt1p2  12440  efi4p  12462  sincossq  12493  cos2tsin  12496  absefi  12514  demoivreALT  12519  p1modz1  12539  dvdsabseq  12592  odd2np1lem  12617  oddp1even  12621  opoe  12640  m1expo  12645  m1exp1  12646  nn0o1gt2  12650  bitsinv1  12707  gcddvds  12718  gcdcl  12721  gcdeq0  12732  gcd0id  12734  bezoutr1  12788  nnmindc  12789  nnminle  12790  eucalg  12815  lcm0val  12821  lcmid  12836  rpmul  12854  dfphi2  12976  phiprmpw  12978  hashgcdeq  12996  odzdvds  13002  nnnn0modprm0  13012  pythagtriplem4  13025  pythagtriplem12  13032  pcaddlem  13096  pcmpt  13100  pockthi  13115  4sqlem12  13159  2expltfac  13196  ballotfilemfp1  13209  ballotfilemfval0  13213  ballotfilemsv  13231  ennnfonelem0  13274  ennnfonelem1  13276  ennnfonelemhdmp1  13278  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemf1  13287  ctiunctlemfo  13308  setsresg  13368  strressid  13402  strle1g  13437  restid2  13579  gzsumwmhm  13780  grplactcnv  13884  mulg0  13905  mulgnn0gzsum  13908  mulgneg  13920  mulgneg2  13936  gzsumconst  14120  gzsumsnfd  14124  gzsumsplit0  14125  gsumvalfi  14129  gsumsncmn  14133  gsump1  14134  gsummptfidmadd  14138  gsummhmfi  14141  prdsbas3  14164  zrhval2  14926  mpl0fi  15016  tgval2  15075  tgidm  15098  epttop  15114  tgrest  15193  restco  15198  restsn  15204  tgcn  15232  cnptopresti  15262  cnptoprest  15263  txbas  15282  upxp  15296  txrest  15300  txdis  15301  txhmeo  15343  txswaphmeolem  15344  xblss2ps  15428  xblss2  15429  qtopbasss  15545  fsumcncntop  15591  hoverb  15672  limcimolemlt  15688  dvcnp2cntop  15723  dvcoapbr  15731  dvexp  15735  dvexp2  15736  dvmptid  15740  dveflem  15750  dvef  15751  plymullem1  15772  plyadd  15775  plymul  15776  plycoeid3  15781  plycjlemc  15784  plycj  15785  sin0pilem1  15805  sin2kpi  15835  cos2kpi  15836  coseq0q4123  15858  coseq0negpitopi  15860  sincosq1eq  15863  sinkpi  15871  coskpi  15872  logfac  15918  1cxp  15925  mpodvdsmulf1o  16018  lgslem2  16034  lgsfcl2  16039  lgs0  16046  lgs2  16050  lgsneg  16057  lgsdilem  16060  lgsdir2lem4  16064  lgsdir2lem5  16065  lgsne0  16071  lgssq  16073  lgssq2  16074  gausslemma2dlem3  16096  gausslemma2dlem4  16097  lgseisenlem1  16103  lgsquadlem2  16111  lgsquad2lem2  16115  lgsquad3  16117  m1lgs  16118  2lgslem1a2  16120  2lgsoddprmlem3  16144  2sqlem9  16157  2sqlem10  16158  edgiedgbg  16220  isuhgrm  16226  isushgrm  16227  uhgr0vb  16239  uhgrun  16241  isupgren  16250  isumgren  16260  umgrnloop0  16272  upgrun  16281  umgrun  16283  isuspgren  16312  isusgren  16313  usgrf1oedg  16360  usgredg3  16369  egrsubgr  16418  0uhgrsubgr  16420  uhgrspansubgrlem  16431  vtxdg0v  16449  vtxdgfi0e  16450  vtxdfifiun  16452  vtxdumgrfival  16453  1loopgrvd2fi  16460  vdegp1cid  16471  wlkl1loop  16513  2wlklem  16531  upgr2wlkdc  16532  clwwlkn0  16563  clwwlkn1  16573  clwwlkn2  16576  umgr2cwwk2dif  16579  clwwlk0on0  16586  clwwlknonel  16587  clwwlknonex2lem1  16592  trlsegvdeglem4  16618  eupthvdres  16630  eupth2lembfi  16632  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  ex-ceil  16654  bj-intexr  16848  peano3nninf  16955  nninfall  16957  isomninnlem  16984  iswomni0  17006  ismkvnnlem  17007  nconstwlpolem0  17018