Theorem eqtrd 2113

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtrd	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtrd

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eqeq2d 2092	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
4	1, 3	mpbid 145	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqtr2d  2114  eqtr3d  2115  eqtr4d  2116  3eqtrd  2117  3eqtrrd  2118  3eqtr2d  2119  syl5eq  2125  syl6eq  2129  rabeqbidv  2596  rabeqbidva  2597  csbidmg  2958  csbco3g  2960  difeq12d  3091  ifeq12d  3368  ifbieq1d  3371  ifbieq2d  3373  ifbieq12d  3375  csbsng  3453  disjpr2  3456  csbunig  3609  iuneq12d  3702  unisn3  4198  op1stbg  4228  opthreg  4299  onsucuni2  4307  csbxpg  4439  coeq12d  4518  csbdmg  4547  dmxpinm  4574  xpid11m  4575  reseq12d  4631  csbresg  4633  resima2  4662  imaeq12d  4689  csbrng  4802  opswapg  4827  relcnvtr  4860  relcoi2  4868  relcoi1  4869  iotaint  4900  funprg  4969  funtpg  4970  funcnvres2  4994  fnco  5027  fococnv2  5172  fveq12d  5204  csbfv12g  5230  csbfv2g  5231  csbfvg  5232  dffn5im  5240  funfvdm2  5258  fvun1  5260  fvmpt2d  5278  fvmptt  5283  fndmin  5295  fniniseg2  5310  fnniniseg2  5311  fmptcof  5352  fvresi  5377  fvunsng  5378  fvpr1g  5388  fvpr2g  5389  fvtp1g  5390  funiunfvdm  5423  fcof1o  5449  riotaeqbidv  5491  oveq123d  5553  csbov12g  5564  csbov1g  5565  csbov2g  5566  ovmpt2dxf  5646  caov42d  5707  caovdilemd  5712  caovimo  5714  grprinvd  5716  offval2  5746  caofinvl  5753  ot1stg  5799  ot2ndg  5800  2nd1st  5826  mpt2mptsx  5843  dmmpt2ssx  5845  fmpt2x  5846  fmpt2co  5857  1stconst  5862  algrflemg  5871  tfrexlem  5971  rdgivallem  5991  rdgisuc1  5994  frec0g  6006  frecsuclem1  6010  frecsuclem3  6013  frecrdg  6015  oa0  6060  oasuc  6067  oa1suc  6070  omsuc  6074  nnaass  6087  nndi  6088  nnmass  6089  nnm2  6121  nn2m  6122  ereq1  6136  errn  6151  uniqs2  6189  oviec  6235  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  phplem4on  6353  fidifsnen  6355  supeq2  6402  eqsupti  6409  infvalti  6435  mulidpi  6508  addasspig  6520  mulasspig  6522  distrpig  6523  indpi  6532  addcmpblnq  6557  mulpipq  6562  dmaddpqlem  6567  nqpi  6568  addcomnqg  6571  recrecnq  6584  ltsonq  6588  ltanqg  6590  ltmnqg  6591  ltaddnq  6597  ltexnqq  6598  archnqq  6607  prarloclemarch  6608  ltrnqg  6610  ltnnnq  6613  nq0nn  6632  addcmpblnq0  6633  nqpnq0nq  6643  nqnq0a  6644  nq0m0r  6646  nq0a0  6647  distrnq0  6649  addassnq0  6652  nq02m  6655  prarloclemlo  6684  prarloclemcalc  6692  addnqprllem  6717  addnqprulem  6718  addnqprl  6719  addnqpru  6720  appdivnq  6753  mulnqprl  6758  mulnqpru  6759  addcanprlemu  6805  ltaprlem  6808  ltmprr  6832  cauappcvgprlemladdrl  6847  mulcmpblnrlemg  6917  mulcomsrg  6934  distrsrg  6936  ltsosr  6941  1idsr  6945  00sr  6946  ltasrg  6947  recexgt0sr  6950  srpospr  6959  prsradd  6962  prsrriota  6964  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsrlemoffres  6976  caucvgsr  6978  elreal2  6999  mulresr  7006  pitonnlem1p1  7014  pitonnlem2  7015  pitoregt0  7017  recidpirqlemcalc  7025  recidpirq  7026  axaddcl  7032  axmulcl  7034  axmulcom  7037  axmulass  7039  axdistr  7040  ax1rid  7043  axcnre  7047  recriota  7056  axcaucvglemcau  7064  mulid1  7116  mulid2  7117  adddirp1d  7145  joinlmuladdmuld  7146  muladd11  7241  1p1times  7242  readdcan  7248  comraddd  7265  add42  7270  npcan  7317  addsubass  7318  2addsub  7322  addsubeq4  7323  nppcan  7330  nnpcan  7331  npncan2  7335  nncan  7337  subsub  7338  nnncan  7343  nnncan1  7344  pnpcan2  7348  pnncan  7349  subneg  7357  negneg  7358  negdi2  7366  mvrraddd  7472  subaddeqd  7473  addid0  7477  mul02  7491  mul01  7493  mulneg1  7499  mul2neg  7502  mulm1  7504  ltadd2  7523  rimul  7685  rereim  7686  mulreim  7704  recextlem1  7741  mulcanapd  7751  divcanap1  7769  divrecap2  7777  divmulassap  7783  divmulasscomap  7784  divcanap4  7787  dividap  7789  muldivdirap  7795  divdivdivap  7801  recdivap  7806  divadddivap  7815  divsubdivap  7816  div2negap  7823  divcanap5rd  7904  dmdcanap2d  7907  recgt0  7928  lt2mul2div  7957  nnmulcl  8060  times2  8161  add1p1  8280  sub1m1  8281  cnm2m1cnm3  8282  nn0supp  8340  peano2z  8387  nneoor  8449  supminfex  8685  cnref1o  8733  rexneg  8897  iooidg  8932  iooval2  8938  icoshftf1o  9013  lincmb01cmp  9025  iccf1o  9026  fzval2  9032  fzsuc  9086  fzpred  9087  fztpval  9100  fseq1p1m1  9111  fzshftral  9125  fzo0to3tp  9228  fzo0sn0fzo1  9230  fzosplitsn  9242  fzosplitprm1  9243  fzisfzounsn  9245  rebtwn2zlemstep  9261  2tnp1ge0ge0  9303  flqdiv  9323  modqvalr  9327  modqdiffl  9337  modqfrac  9339  modqmulnn  9344  modqid  9351  modqcyc  9361  modqcyc2  9362  mulp1mod1  9367  modqmuladd  9368  modqmuladdnn0  9370  qnegmod  9371  m1modnnsub1  9372  addmodid  9374  addmodidr  9375  modqmul12d  9380  modqnegd  9381  modqadd12d  9382  modifeq2int  9388  modqaddmulmod  9393  modqdi  9394  modqsubdir  9395  modsumfzodifsn  9398  addmodlteq  9400  frec2uzsucd  9403  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdglem  9413  frecuzrdgsuc  9417  frecfzennn  9419  iseqeq1  9434  iseqp1  9445  iseqfeq2  9449  iseqfveq  9450  iseqshft2  9452  iseq1p  9459  iseqid3s  9466  iseqz  9469  expivallem  9477  expinnval  9479  expp1  9483  expn1ap0  9486  mulexp  9515  expaddzaplem  9519  expaddzap  9520  expmul  9521  expp1zap  9525  expm1ap  9526  sqval  9534  iexpcyc  9579  subsq2  9582  binom2  9585  binom21  9586  mulbinom2  9589  binom3  9590  zesq  9591  bernneq  9593  sqoddm1div8  9625  nn0opthlem1d  9647  facp1  9657  faclbnd6  9671  bcval2  9677  bcval3  9678  bcn0  9682  bcp1n  9688  bcp1nk  9689  bcn2  9691  bcp1m1  9692  bcpasc  9693  bcn2m1  9696  shftdm  9710  shftval2  9714  shftval4  9716  shftval5  9717  shftcan1  9722  imre  9738  crre  9744  remim  9747  reim0b  9749  recj  9754  reneg  9755  readd  9756  resub  9757  remullem  9758  imcj  9762  imneg  9763  imadd  9764  imsub  9765  cjcj  9770  cjadd  9771  ipcnval  9773  cjneg  9777  cjsub  9779  cjexp  9780  imval2  9781  cjap  9793  resqrexlemf1  9894  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  resqrtcl  9915  sqrtsq  9930  absneg  9936  absvalsq  9939  absvalsq2  9940  sqabsadd  9941  sqabssub  9942  absval2  9943  absreimsq  9953  absmul  9955  absexp  9965  absexpzap  9966  abssuble0  9989  abstri  9990  recan  9995  amgm2  10004  maxabslemlub  10093  max0addsup  10105  minmax  10112  climshft2  10145  subcn2  10150  climaddc2  10168  clim2iser2  10176  climcvg1nlem  10186  dvdstr  10232  dvdsadd2b  10242  mulmoddvds  10263  ltoddhalfle  10293  opoe  10295  m1expo  10300  m1exp1  10301  flodddiv4  10334  flodddiv4t2lthalf  10337  zsupcllemstep  10341  nn0gcdid0  10372  gcdaddm  10375  gcdadd  10376  gcdid  10377  gcdabs  10379  modgcd  10382  1gcd  10383  bezout  10400  dfgcd2  10403  mulgcd  10405  absmulgcd  10406  gcdmultiple  10409  gcdmultiplez  10410  rpmulgcd  10415  rplpwr  10416  rppwr  10417  dvdssqlem  10419  ialgr0  10426  ialginv  10429  ialgcvg  10430  ialgfx  10434  eucalginv  10438  eucalglt  10439  lcmcl  10454  lcmabs  10458  lcmgcdlem  10459  lcmdvds  10461  lcmgcdnn  10464  coprmdvds  10474  qredeq  10478  divgcdcoprm0  10483  divgcdcoprmex  10484  rpexp1i  10533  sqrt2irrlem  10540  sqpweven  10553  2sqpwodd  10554  sqrt2irraplemnn  10557  qdencn  10785