Theorem eqtrd 2117

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 2096	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
4	1, 3	mpbid 145	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1287

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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067

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

This theorem is referenced by:  eqtr2d  2118  eqtr3d  2119  eqtr4d  2120  3eqtrd  2121  3eqtrrd  2122  3eqtr2d  2123  syl5eq  2129  syl6eq  2133  rabeqbidv  2610  rabeqbidva  2611  csbidmg  2973  csbco3g  2975  difeq12d  3108  ifeq12d  3396  ifbieq1d  3399  ifbieq2d  3401  ifbieq12d  3403  eqifdc  3411  csbsng  3488  disjpr2  3491  csbunig  3646  iuneq12d  3739  unisn3  4246  op1stbg  4276  opthreg  4347  onsucuni2  4355  csbxpg  4489  coeq12d  4570  csbdmg  4600  dmxpinm  4627  xpid11m  4628  reseq12d  4684  csbresg  4686  resima2  4715  imaeq12d  4744  csbrng  4860  opswapg  4885  relcnvtr  4918  relcoi2  4929  relcoi1  4930  iotaint  4961  funprg  5031  funtpg  5032  funcnvres2  5056  fnco  5089  fococnv2  5244  fveq12d  5277  csbfv12g  5305  csbfv2g  5306  csbfvg  5307  dffn5im  5315  funfvdm2  5333  fvun1  5335  fvmpt2d  5354  fvmptt  5359  fndmin  5371  fniniseg2  5386  fnniniseg2  5387  fmptcof  5430  fvresi  5455  fvunsng  5456  fvpr1g  5466  fvpr2g  5467  fvtp1g  5468  funiunfvdm  5505  fcof1o  5531  riotaeqbidv  5574  oveq123d  5636  csbov12g  5647  csbov1g  5648  csbov2g  5649  ovmpt2dxf  5729  caov42d  5790  caovdilemd  5795  caovimo  5797  grprinvd  5799  offval2  5829  caofinvl  5836  ot1stg  5882  ot2ndg  5883  2nd1st  5909  mpt2mptsx  5926  dmmpt2ssx  5928  fmpt2x  5929  fmpt2co  5940  1stconst  5945  algrflemg  5954  tfrexlem  6055  rdgivallem  6102  rdgisuc1  6105  frec0g  6118  frecabcl  6120  frecsuclem  6127  frecrdg  6129  oa0  6174  oasuc  6181  oa1suc  6184  omsuc  6189  nnaass  6202  nndi  6203  nnmass  6204  nnm2  6238  nn2m  6239  ereq1  6253  errn  6268  uniqs2  6306  oviec  6352  ecovass  6355  ecoviass  6356  ecovdi  6357  ecovidi  6358  mapsnconst  6405  mapen  6516  mapxpen  6518  xpmapenlem  6519  phplem4on  6537  fidifsnen  6540  undifdc  6588  fisseneq  6595  snexxph  6611  sbthlemi4  6616  sbthlemi6  6618  supeq2  6631  eqsupti  6638  infvalti  6664  djuf1olem  6692  djuss  6708  1stinl  6712  2ndinl  6713  1stinr  6714  2ndinr  6715  updjudhcoinlf  6718  updjudhcoinrg  6719  en2other2  6769  mulidpi  6824  addasspig  6836  mulasspig  6838  distrpig  6839  indpi  6848  addcmpblnq  6873  mulpipq  6878  dmaddpqlem  6883  nqpi  6884  addcomnqg  6887  recrecnq  6900  ltsonq  6904  ltanqg  6906  ltmnqg  6907  ltaddnq  6913  ltexnqq  6914  archnqq  6923  prarloclemarch  6924  ltrnqg  6926  ltnnnq  6929  nq0nn  6948  addcmpblnq0  6949  nqpnq0nq  6959  nqnq0a  6960  nq0m0r  6962  nq0a0  6963  distrnq0  6965  addassnq0  6968  nq02m  6971  prarloclemlo  7000  prarloclemcalc  7008  addnqprllem  7033  addnqprulem  7034  addnqprl  7035  addnqpru  7036  appdivnq  7069  mulnqprl  7074  mulnqpru  7075  addcanprlemu  7121  ltaprlem  7124  ltmprr  7148  cauappcvgprlemladdrl  7163  mulcmpblnrlemg  7233  mulcomsrg  7250  distrsrg  7252  ltsosr  7257  1idsr  7261  00sr  7262  ltasrg  7263  recexgt0sr  7266  srpospr  7275  prsradd  7278  prsrriota  7280  caucvgsrlemcau  7285  caucvgsrlemgt1  7287  caucvgsrlemoffval  7288  caucvgsrlemoffres  7292  caucvgsr  7294  elreal2  7315  mulresr  7322  pitonnlem1p1  7330  pitonnlem2  7331  pitoregt0  7333  recidpirqlemcalc  7341  recidpirq  7342  axaddcl  7348  axmulcl  7350  axmulcom  7353  axmulass  7355  axdistr  7356  ax1rid  7359  axcnre  7363  recriota  7372  axcaucvglemcau  7380  mulid1  7432  mulid2  7433  adddirp1d  7461  joinlmuladdmuld  7462  muladd11  7562  1p1times  7563  readdcan  7569  comraddd  7586  add42  7591  npcan  7638  addsubass  7639  2addsub  7643  addsubeq4  7644  nppcan  7651  nnpcan  7652  npncan2  7656  nncan  7658  subsub  7659  nnncan  7664  nnncan1  7665  pnpcan2  7669  pnncan  7670  subneg  7678  negneg  7679  negdi2  7687  mvrraddd  7793  subaddeqd  7794  addid0  7798  mul02  7812  mul01  7814  mulneg1  7820  mul2neg  7823  mulm1  7825  ltadd2  7844  rimul  8006  rereim  8007  mulreim  8025  recextlem1  8062  mulcanapd  8072  divcanap1  8090  divrecap2  8098  divmulassap  8104  divmulasscomap  8105  divcanap4  8108  dividap  8110  muldivdirap  8116  divdivdivap  8122  recdivap  8127  divadddivap  8136  divsubdivap  8137  div2negap  8144  divcanap5rd  8225  dmdcanap2d  8228  recgt0  8249  lt2mul2div  8278  nnmulcl  8381  times2  8482  add1p1  8601  sub1m1  8602  cnm2m1cnm3  8603  nn0supp  8661  peano2z  8722  nneoor  8784  supminfex  9020  cnref1o  9068  rexneg  9227  iooidg  9262  iooval2  9268  icoshftf1o  9343  lincmb01cmp  9355  iccf1o  9356  fzval2  9362  fzsuc  9416  fzpred  9417  fztpval  9430  fseq1p1m1  9441  fzshftral  9455  fzo0to3tp  9561  fzo0sn0fzo1  9563  fzosplitsn  9575  fzosplitprm1  9576  fzisfzounsn  9578  rebtwn2zlemstep  9595  2tnp1ge0ge0  9639  flqdiv  9659  modqvalr  9663  modqdiffl  9673  modqfrac  9675  modqmulnn  9680  modqid  9687  modqcyc  9697  modqcyc2  9698  mulp1mod1  9703  modqmuladd  9704  modqmuladdnn0  9706  qnegmod  9707  m1modnnsub1  9708  addmodid  9710  addmodidr  9711  modqmul12d  9716  modqnegd  9717  modqadd12d  9718  modifeq2int  9724  modqaddmulmod  9729  modqdi  9730  modqsubdir  9731  modsumfzodifsn  9734  addmodlteq  9736  frec2uzsucd  9739  frecuzrdgrrn  9746  frec2uzrdg  9747  frecuzrdglem  9749  frecuzrdgsuc  9752  frecuzrdgg  9754  frecuzrdgdomlem  9755  frecuzrdgfunlem  9757  frecuzrdgtclt  9759  frecuzrdgsuctlem  9761  frecfzennn  9764  iseqeq1  9788  iseqvalt  9804  iseqp1  9812  iseqp1t  9813  iseqoveq  9816  iseqfeq2  9821  iseqfveq  9822  iseqshft2  9824  iseq1p  9833  iseqf1olemnab  9841  iseqf1olemab  9842  iseqf1olemnanb  9843  iseqf1olemqk  9847  iseqf1olemfvp  9850  iseqf1olemqsumkj  9851  iseqf1olemqsumk  9852  iseqf1olemqsum  9853  iseqf1o  9857  iseqid3s  9861  iseqz  9865  fser0const  9871  expivallem  9876  expinnval  9878  expp1  9882  expn1ap0  9885  mulexp  9914  expaddzaplem  9918  expaddzap  9919  expmul  9920  expp1zap  9924  expm1ap  9925  sqval  9933  iexpcyc  9978  subsq2  9981  binom2  9984  binom21  9985  mulbinom2  9988  binom3  9989  zesq  9990  bernneq  9992  sqoddm1div8  10024  nn0opthlem1d  10046  facp1  10056  faclbnd6  10070  bcval2  10076  bcval3  10077  bcn0  10081  bcp1n  10087  bcp1nk  10088  bcn2  10090  bcp1m1  10091  bcpasc  10092  bcn2m1  10095  hashinfom  10104  hashennn  10106  hashfz1  10109  fseq1hash  10127  omgadd  10128  hashunsng  10133  hashprg  10134  hashdifsn  10145  hashdifpr  10146  hashfz  10147  hashfzo  10148  hashfzo0  10149  hashfzp1  10150  hashfz0  10151  hashxp  10152  resunimafz0  10154  fnfz0hash  10155  ffzo0hash  10157  hashfacen  10159  zfz1isolemsplit  10161  zfz1isolemiso  10162  zfz1isolem1  10163  shftdm  10174  shftval2  10178  shftval4  10180  shftval5  10181  shftcan1  10186  imre  10202  crre  10208  remim  10211  reim0b  10213  recj  10218  reneg  10219  readd  10220  resub  10221  remullem  10222  imcj  10226  imneg  10227  imadd  10228  imsub  10229  cjcj  10234  cjadd  10235  ipcnval  10237  cjneg  10241  cjsub  10243  cjexp  10244  imval2  10245  cjap  10257  resqrexlemf1  10358  resqrexlemfp1  10359  resqrexlemover  10360  resqrexlemcalc1  10364  resqrexlemcalc3  10366  resqrexlemnm  10368  resqrexlemcvg  10369  resqrtcl  10379  sqrtsq  10394  absneg  10400  absvalsq  10403  absvalsq2  10404  sqabsadd  10405  sqabssub  10406  absval2  10407  absreimsq  10417  absmul  10419  absexp  10429  absexpzap  10430  abssuble0  10453  abstri  10454  recan  10459  amgm2  10468  maxabslemlub  10557  max0addsup  10569  minmax  10577  climshft2  10611  subcn2  10616  climaddc2  10634  climcvg1nlem  10652  sumeq12dv  10675  sumeq12rdv  10676  isumrblem  10679  fisumcvg  10680  isummolem3  10683  isummolem2a  10684  isummo  10686  fisum  10689  isumz  10691  fsumf1o  10692  fisumss  10694  fisumsers  10697  fsumsplit  10708  fsumsplitf  10709  sumsnf  10710  fsum1  10712  sumpr  10713  sumtp  10714  fsumm1  10716  fsum1p  10718  fsumsplitsnun  10719  fsump1  10720  dvdstr  10758  dvdsadd2b  10768  mulmoddvds  10789  ltoddhalfle  10818  opoe  10820  m1expo  10825  m1exp1  10826  flodddiv4  10859  flodddiv4t2lthalf  10862  zsupcllemstep  10866  nn0gcdid0  10897  gcdaddm  10900  gcdadd  10901  gcdid  10902  gcdabs  10904  modgcd  10907  1gcd  10908  bezout  10925  dfgcd2  10928  mulgcd  10930  absmulgcd  10931  gcdmultiple  10934  gcdmultiplez  10935  rpmulgcd  10940  rplpwr  10941  rppwr  10942  dvdssqlem  10944  ialgr0  10951  ialginv  10954  ialgcvg  10955  ialgfx  10959  eucalginv  10963  eucalglt  10964  lcmcl  10979  lcmabs  10983  lcmgcdlem  10984  lcmdvds  10986  lcmgcdnn  10989  coprmdvds  10999  qredeq  11003  divgcdcoprm0  11008  divgcdcoprmex  11009  rpexp1i  11058  sqrt2irrlem  11065  sqpweven  11078  2sqpwodd  11079  sqrt2irraplemnn  11082  qmuldeneqnum  11098  nn0gcdsq  11103  numdensq  11105  nn0sqrtelqelz  11109  phibndlem  11117  dfphi2  11121  phiprmpw  11123  phiprm  11124  phimullem  11126  hashgcdlem  11128  djucllem  11188  nninfalllemn  11386  nninfsellemeq  11394  qdencn  11403