Theorem eqtrd 2132

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

Syntax hints:   → wi 4   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  eqtr2d  2133  eqtr3d  2134  eqtr4d  2135  3eqtrd  2136  3eqtrrd  2137  3eqtr2d  2138  syl5eq  2144  syl6eq  2148  rabeqbidv  2636  rabeqbidva  2637  csbidmg  3006  csbco3g  3008  difeq12d  3142  ifeq12d  3438  ifbieq1d  3441  ifbieq2d  3443  ifbieq12d  3445  eqifdc  3453  csbsng  3531  disjpr2  3534  csbunig  3691  iuneq12d  3784  unisn3  4304  op1stbg  4338  opthreg  4409  onsucuni2  4417  csbxpg  4558  coeq12d  4641  csbdmg  4671  reseq12d  4756  csbresg  4758  resima2  4789  imaeq12d  4818  csbrng  4936  opswapg  4961  relcnvtr  4994  relcoi2  5005  relcoi1  5006  iotaint  5037  funprg  5109  funtpg  5110  funcnvres2  5134  fnco  5167  fococnv2  5327  fveq12d  5360  csbfv12g  5389  csbfv2g  5390  csbfvg  5391  dffn5im  5399  funfvdm2  5417  fvun1  5419  fvmpt2d  5439  fvmptt  5444  fndmin  5459  fniniseg2  5474  fnniniseg2  5475  fmptcof  5519  fvresi  5545  fvunsng  5546  fvpr1g  5558  fvpr2g  5559  fvtp1g  5560  funiunfvdm  5596  fcof1o  5622  riotaeqbidv  5665  oveq123d  5727  csbov12g  5742  csbov1g  5743  csbov2g  5744  ovmpodxf  5828  caov42d  5889  caovdilemd  5894  caovimo  5896  grprinvd  5898  offval2  5928  caofinvl  5935  ot1stg  5981  ot2ndg  5982  2nd1st  6008  mpomptsx  6025  dmmpossx  6027  fmpox  6028  fmpoco  6043  1stconst  6048  algrflemg  6057  tfrexlem  6161  rdgivallem  6208  rdgisuc1  6211  frec0g  6224  frecabcl  6226  frecsuclem  6233  frecrdg  6235  oa0  6283  oasuc  6290  oa1suc  6293  omsuc  6298  nnaass  6311  nndi  6312  nnmass  6313  nnm2  6351  nn2m  6352  ereq1  6366  errn  6381  uniqs2  6419  oviec  6465  ecovass  6468  ecoviass  6469  ecovdi  6470  ecovidi  6471  mapsnconst  6518  mapen  6669  mapxpen  6671  xpmapenlem  6672  phplem4on  6690  fidifsnen  6693  undifdc  6741  fiintim  6746  fisseneq  6749  snexxph  6766  sbthlemi4  6776  sbthlemi6  6778  supeq2  6791  eqsupti  6798  infvalti  6824  djuf1olem  6853  djuss  6870  1stinl  6874  2ndinl  6875  1stinr  6876  2ndinr  6877  updjudhcoinlf  6880  updjudhcoinrg  6881  omp1eomlem  6894  difinfsn  6900  ctmlemr  6908  ctssdclemn0  6910  ctssdc  6912  enumctlemm  6913  en2other2  6961  mulidpi  7027  addasspig  7039  mulasspig  7041  distrpig  7042  indpi  7051  addcmpblnq  7076  mulpipq  7081  dmaddpqlem  7086  nqpi  7087  addcomnqg  7090  recrecnq  7103  ltsonq  7107  ltanqg  7109  ltmnqg  7110  ltaddnq  7116  ltexnqq  7117  archnqq  7126  prarloclemarch  7127  ltrnqg  7129  ltnnnq  7132  nq0nn  7151  addcmpblnq0  7152  nqpnq0nq  7162  nqnq0a  7163  nq0m0r  7165  nq0a0  7166  distrnq0  7168  addassnq0  7171  nq02m  7174  prarloclemlo  7203  prarloclemcalc  7211  addnqprllem  7236  addnqprulem  7237  addnqprl  7238  addnqpru  7239  appdivnq  7272  mulnqprl  7277  mulnqpru  7278  addcanprlemu  7324  ltaprlem  7327  ltmprr  7351  cauappcvgprlemladdrl  7366  mulcmpblnrlemg  7436  mulcomsrg  7453  distrsrg  7455  ltsosr  7460  1idsr  7464  00sr  7465  ltasrg  7466  recexgt0sr  7469  srpospr  7478  prsradd  7481  prsrriota  7483  caucvgsrlemcau  7488  caucvgsrlemgt1  7490  caucvgsrlemoffval  7491  caucvgsrlemoffres  7495  caucvgsr  7497  elreal2  7518  mulresr  7525  pitonnlem1p1  7533  pitonnlem2  7534  pitoregt0  7536  recidpirqlemcalc  7544  recidpirq  7545  axaddcl  7551  axmulcl  7553  axmulcom  7556  axmulass  7558  axdistr  7559  ax1rid  7562  axcnre  7566  recriota  7575  axcaucvglemcau  7583  mulid1  7635  mulid2  7636  adddirp1d  7664  joinlmuladdmuld  7665  muladd11  7766  1p1times  7767  readdcan  7773  comraddd  7790  add42  7795  npcan  7842  addsubass  7843  2addsub  7847  addsubeq4  7848  nppcan  7855  nnpcan  7856  npncan2  7860  nncan  7862  subsub  7863  nnncan  7868  nnncan1  7869  pnpcan2  7873  pnncan  7874  subneg  7882  negneg  7883  negdi2  7891  mvrraddd  7997  subaddeqd  7998  addid0  8002  mul02  8016  mul01  8018  mulneg1  8024  mul2neg  8027  mulm1  8029  ltadd2  8048  rimul  8213  rereim  8214  mulreim  8232  recextlem1  8273  mulcanapd  8283  divcanap1  8302  divrecap2  8310  divmulassap  8316  divmulasscomap  8317  divcanap4  8320  dividap  8322  muldivdirap  8328  divdivdivap  8334  recdivap  8339  divadddivap  8348  divsubdivap  8349  div2negap  8356  divcanap5rd  8439  dmdcanap2d  8442  recgt0  8466  lt2mul2div  8495  nnmulcl  8599  times2  8701  add1p1  8821  sub1m1  8822  cnm2m1cnm3  8823  nn0supp  8881  peano2z  8942  nneoor  9005  supminfex  9242  cnref1o  9290  rexneg  9454  xaddpnf1  9470  xaddmnf1  9472  rexadd  9476  xaddid1  9486  xaddid2  9487  xaddass  9493  xpncan  9495  xleadd1a  9497  xltadd1  9500  xposdif  9506  xadd4d  9509  xleaddadd  9511  iooidg  9533  iooval2  9539  icoshftf1o  9615  lincmb01cmp  9627  iccf1o  9628  fzval2  9634  fzsuc  9690  fzpred  9691  fztpval  9704  fseq1p1m1  9715  fzshftral  9729  fzo0to3tp  9837  fzo0sn0fzo1  9839  fzosplitsn  9851  fzosplitprm1  9852  fzisfzounsn  9854  rebtwn2zlemstep  9871  2tnp1ge0ge0  9915  flqdiv  9935  modqvalr  9939  modqdiffl  9949  modqfrac  9951  modqmulnn  9956  modqid  9963  modqcyc  9973  modqcyc2  9974  mulp1mod1  9979  modqmuladd  9980  modqmuladdnn0  9982  qnegmod  9983  m1modnnsub1  9984  addmodid  9986  addmodidr  9987  modqmul12d  9992  modqnegd  9993  modqadd12d  9994  modifeq2int  10000  modqaddmulmod  10005  modqdi  10006  modqsubdir  10007  modsumfzodifsn  10010  addmodlteq  10012  frec2uzsucd  10015  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdglem  10025  frecuzrdgsuc  10028  frecuzrdgg  10030  frecuzrdgdomlem  10031  frecuzrdgfunlem  10033  frecuzrdgtclt  10035  frecuzrdgsuctlem  10037  frecfzennn  10040  seqeq1  10062  seq3val  10072  seqvalcd  10073  seq3p1  10076  seqp1cd  10080  seq3feq2  10084  seq3fveq  10085  seq3shft2  10087  seq3-1p  10094  iseqf1olemnab  10102  iseqf1olemab  10103  iseqf1olemnanb  10104  iseqf1olemqk  10108  iseqf1olemfvp  10111  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3f1o  10118  seq3id3  10121  seq3z  10125  fser0const  10130  exp3vallem  10135  expnnval  10137  expp1  10141  expn1ap0  10144  mulexp  10173  expaddzaplem  10177  expaddzap  10178  expmul  10179  expp1zap  10183  expm1ap  10184  sqval  10192  iexpcyc  10238  subsq2  10241  binom2  10244  binom21  10245  binom2sub1  10247  mulbinom2  10249  binom3  10250  zesq  10251  bernneq  10253  sqoddm1div8  10285  nn0opthlem1d  10307  facp1  10317  faclbnd6  10331  bcval2  10337  bcval3  10338  bcn0  10342  bcp1n  10348  bcp1nk  10349  bcn2  10351  bcp1m1  10352  bcpasc  10353  bcn2m1  10356  hashinfom  10365  hashennn  10367  hashfz1  10370  fseq1hash  10388  omgadd  10389  hashunsng  10394  hashprg  10395  hashdifsn  10406  hashdifpr  10407  hashfz  10408  hashfzo  10409  hashfzo0  10410  hashfzp1  10411  hashfz0  10412  hashxp  10413  resunimafz0  10415  fnfz0hash  10416  ffzo0hash  10418  hashfacen  10420  zfz1isolemsplit  10422  zfz1isolemiso  10423  zfz1isolem1  10424  shftdm  10435  shftval2  10439  shftval4  10441  shftval5  10442  shftcan1  10447  seq3shft  10451  imre  10464  crre  10470  remim  10473  reim0b  10475  recj  10480  reneg  10481  readd  10482  resub  10483  remullem  10484  imcj  10488  imneg  10489  imadd  10490  imsub  10491  cjcj  10496  cjadd  10497  ipcnval  10499  cjneg  10503  cjsub  10505  cjexp  10506  imval2  10507  cjap  10519  resqrexlemf1  10620  resqrexlemfp1  10621  resqrexlemover  10622  resqrexlemcalc1  10626  resqrexlemcalc3  10628  resqrexlemnm  10630  resqrexlemcvg  10631  resqrtcl  10641  sqrtsq  10656  absneg  10662  absvalsq  10665  absvalsq2  10666  sqabsadd  10667  sqabssub  10668  absval2  10669  absreimsq  10679  absmul  10681  absexp  10691  absexpzap  10692  abssuble0  10715  abstri  10716  recan  10721  amgm2  10730  maxabslemlub  10819  max0addsup  10831  minmax  10840  minabs  10846  bdtrilem  10849  bdtri  10850  xrmaxiflemab  10855  xrmaxiflemcom  10857  xrmaxadd  10869  xrminmax  10873  xrmineqinf  10877  xrminrecl  10881  xrbdtri  10884  climshft2  10914  subcn2  10919  reccn2ap  10921  climaddc2  10938  iser3shft  10954  climcvg1nlem  10957  sumeq12dv  10980  sumeq12rdv  10981  sumrbdclem  10984  fsum3cvg  10985  summodclem3  10988  summodclem2a  10989  summodc  10991  fsum3  10995  isumz  10997  fsumf1o  10998  fisumss  11000  fsumsersdc  11003  fsum3ser  11005  fsumsplit  11015  fsumsplitf  11016  sumsnf  11017  fsumsplitsn  11018  fsum1  11020  sumpr  11021  sumtp  11022  fsumm1  11024  fsum1p  11026  fsumsplitsnun  11027  fsump1  11028  isumclim  11029  sumnul  11032  isumadd  11039  fsum2dlemstep  11042  fsumcnv  11045  fisumcom2  11046  fsumshftm  11053  fisumrev2  11054  fisum0diag2  11055  fsumsub  11060  fsumdifsnconst  11063  modfsummodlemstep  11065  fsumabs  11073  telfsumo  11074  telfsum  11076  telfsum2  11077  fsumparts  11078  fsumiun  11085  hashiun  11086  hash2iun  11087  hash2iun1dif1  11088  binomlem  11091  binom1p  11093  binom11  11094  binom1dif  11095  bcxmas  11097  isum1p  11100  isumnn0nn  11101  isumlessdc  11104  divcnv  11105  arisum2  11107  trireciplem  11108  geosergap  11114  geolim  11119  georeclim  11121  geo2lim  11124  geoisum1  11127  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  cvgratnnlemsumlt  11136  cvgratz  11140  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  eftabs  11160  efcllemp  11162  ef0lem  11164  efcvgfsum  11171  ege2le3  11175  efcj  11177  efaddlem  11178  efexp  11186  eftlub  11194  efsep  11195  effsumlt  11196  ef4p  11198  efgt1p2  11199  efgt1p  11200  tanval2ap  11218  tanval3ap  11219  resinval  11220  recosval  11221  efi4p  11222  resin4p  11223  recos4p  11224  sinneg  11231  cosneg  11232  tannegap  11233  efmival  11238  sinadd  11241  cosadd  11242  tanaddaplem  11243  tanaddap  11244  sinsub  11245  cossub  11246  addsin  11247  subsin  11248  subcos  11252  sincossq  11253  sin2t  11254  sin01bnd  11262  cos01bnd  11263  absefi  11272  absef  11273  absefib  11274  efieq1re  11275  demoivre  11276  demoivreALT  11277  eirraplem  11278  dvdstr  11325  dvdsadd2b  11335  mulmoddvds  11356  ltoddhalfle  11385  opoe  11387  m1expo  11392  m1exp1  11393  flodddiv4  11426  flodddiv4t2lthalf  11429  zsupcllemstep  11433  nn0gcdid0  11464  gcdaddm  11467  gcdadd  11468  gcdid  11469  gcdabs  11471  modgcd  11474  1gcd  11475  bezout  11492  dfgcd2  11495  mulgcd  11497  absmulgcd  11498  gcdmultiple  11501  gcdmultiplez  11502  rpmulgcd  11507  rplpwr  11508  rppwr  11509  dvdssqlem  11511  ialgr0  11518  alginv  11521  algcvg  11522  algfx  11526  eucalginv  11530  eucalglt  11531  lcmcl  11546  lcmabs  11550  lcmgcdlem  11551  lcmdvds  11553  lcmgcdnn  11556  coprmdvds  11566  qredeq  11570  divgcdcoprm0  11575  divgcdcoprmex  11576  rpexp1i  11625  sqrt2irrlem  11632  sqpweven  11645  2sqpwodd  11646  sqrt2irraplemnn  11649  qmuldeneqnum  11665  nn0gcdsq  11670  numdensq  11672  nn0sqrtelqelz  11676  phibndlem  11684  dfphi2  11688  phiprmpw  11690  phiprm  11691  phimullem  11693  hashgcdlem  11695  ennnfonelemp1  11711  ennnfonelemhdmp1  11714  ennnfonelemss  11715  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemhom  11720  ennnfonelemnn0  11727  ctinfomlemom  11732  setsvala  11772  fvsetsid  11775  setsresg  11779  setscom  11781  setsslid  11791  ressid2  11800  ressval2  11801  restid2  11911  ntrval  12061  clsval  12062  cldcls  12065  neival  12094  resttop  12121  restco  12125  restabs  12126  resttopon2  12129  cnpval  12148  cnntr  12175  cnrest2  12186  upxp  12222  uptx  12224  cnmpt11  12233  cnmpt21  12241  psmetsym  12257  psmetres2  12261  xmetsym  12296  cnbl0  12456  cnblcld  12457  remetdval  12458  bl2ioo  12461  tgioo  12465  cncfmet  12492  cncfmptc  12495  addccncf  12498  negcncf  12500  mulcncflem  12502  limcimolemlt  12513  cnplimcim  12516  dvfvalap  12523  dvconst  12534  djucllem  12588  nninfalllemn  12786  nninfsellemeq  12794  nninffeq  12800  qdencn  12806  cvgcmp2nlemabs  12811  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818