Theorem eqtr3d 2175

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

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

Assertion

Ref	Expression
eqtr3d	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2146	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqtr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtrd 2173	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  3eqtr3d  2181  3eqtr3rd  2182  3eqtr3a  2197  opth  4167  eusvnf  4382  f00  5322  f1imacnv  5392  foimacnv  5393  f1ococnv1  5404  funfvdm  5492  fvmptdf  5516  fndmdif  5533  acexmidlemph  5775  acexmidlemab  5776  ovmpodf  5910  oprssov  5920  grpridd  5975  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  oav2  6367  omv2  6369  fnsnsplitdc  6409  ecopovtrn  6534  ecopovtrng  6537  map0b  6589  en1  6701  ssenen  6753  fidifsnen  6772  dif1en  6781  undifdc  6820  fidcenumlemr  6851  ordiso2  6928  finomni  7020  exmidomni  7022  fodjum  7026  exmidaclem  7081  distrnqg  7219  1qec  7220  prarloclemarch2  7251  nnnq0lem1  7278  nqpnq0nq  7285  distrnq0  7291  prarloclemlt  7325  prmuloclemcalc  7397  ltaprg  7451  prplnqu  7452  recexprlem1ssl  7465  recexprlem1ssu  7466  ltmprr  7474  cauappcvgprlemopl  7478  caucvgprlemopl  7501  caucvgprprlemopl  7529  caucvgprprlemexb  7539  prsrlem1  7574  ltsosr  7596  mulgt0sr  7610  recidpipr  7688  recriota  7722  nntopi  7726  axcaucvglemres  7731  addid2  7925  readdcan  7926  muladd11r  7942  add32r  7946  cnegexlem2  7962  cnegex  7964  pncan2  7993  addsubass  7996  subadd23  7998  addsub12  7999  subid  8005  subid1  8006  npncan  8007  nppcan3  8010  subsub  8016  nppcan2  8017  nnncan2  8023  npncan3  8024  pnpcan  8025  negdi  8043  mvlraddd  8150  mvlladdd  8151  pnpncand  8161  subdi  8171  mulsub  8187  mulsub2  8188  eqord1  8269  recexap  8438  div32ap  8476  divsubdirap  8492  divmuldivap  8496  divdivdivap  8497  divmuleqap  8501  divcanap6  8503  dmdcanap  8506  divsubdivap  8512  div2negap  8519  div2subap  8620  mvllmulapd  8625  prodgt0gt0  8633  cju  8743  zneo  9176  infrenegsupex  9416  qreccl  9461  mul2lt0rlt0  9576  xnpcan  9685  fzosn  10013  modqid  10153  modqm1p1mod0  10179  modqltm1p1mod  10180  modqmul1  10181  modaddmodup  10191  modaddmodlo  10192  modqsubdir  10197  iseqf1olemkle  10288  iseqf1olemklt  10289  seq3f1olemstep  10305  seq3f1oleml  10307  seqfeq3  10316  seq3distr  10317  expineg2  10333  expm1t  10352  expadd  10366  expaddzaplem  10367  expmulzap  10370  sqsubswap  10384  subsq2  10431  binom2sub  10436  binom3  10440  facndiv  10517  bcval5  10541  bcn2p1  10548  bcnm1  10550  2shfti  10635  shftcan2  10639  reim0  10665  imval2  10698  cjreim2  10708  cjdivap  10713  cnrecnv  10714  rennim  10806  resqrexlemnm  10822  remsqsqrt  10836  sqrtdiv  10846  sqrtmsq  10849  sqabsadd  10859  sqabssub  10860  absreim  10872  absdivap  10874  absnid  10877  sqabs  10886  abslt  10892  absle  10893  recvalap  10901  abssub  10905  maxabslemlub  11011  infxrnegsupex  11064  mulcn2  11113  reccn2ap  11114  cjcn2  11117  summodclem3  11181  summodclem2a  11182  summodc  11184  zsumdc  11185  fsum3  11188  fisumss  11193  fsumcl2lem  11199  fsumm1  11217  fsum1p  11219  isummulc2  11227  telfsumo  11267  binomlem  11284  bcxmas  11290  arisum  11299  trireciplem  11301  trirecip  11302  geolim2  11313  georeclim  11314  cvgratnnlemfm  11330  cvgratz  11333  mertenslemi1  11336  clim2divap  11341  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  efcan  11419  efexp  11425  efzval  11426  efgt0  11427  eftlub  11433  efltim  11441  resinval  11458  recosval  11459  cosmul  11488  cos2t  11493  cos2tsin  11494  cos01bnd  11501  cos12dec  11510  eirraplem  11519  muldvds1  11554  dvdsexp  11595  oexpneg  11610  divalglemqt  11652  divalglemeunn  11654  divalglemeuneg  11656  divalgmod  11660  flodddiv4t2lthalf  11670  gcdid0  11704  gcdaddm  11708  dvdsgcdidd  11718  rpmulgcd  11750  sqgcd  11753  algcvg  11765  eucalgcvga  11775  eucalg  11776  dvdslcm  11786  lcmeq0  11788  lcmgcd  11795  qredeu  11814  sqnprm  11852  divgcdodd  11857  sqrt2irrlem  11875  sqpweven  11889  2sqpwodd  11890  divnumden  11910  hashdvds  11933  phimullem  11937  ennnfonelemhf1o  11962  strslssd  12044  topnidg  12172  restopnb  12389  txcnmpt  12481  cnmpt1t  12493  blhalf  12616  xmspropd  12685  mspropd  12686  limcimolemlt  12841  dvfre  12882  dveflem  12895  dvef  12896  sin2kpi  12940  cos2kpi  12941  sin2pim  12942  cos2pim  12943  ptolemy  12953  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  tangtx  12967  sincosq1eq  12968  abssinper  12975  sinkpi  12976  relogeftb  12994  relogoprlem  12997  relogexp  13001  peano3nninf  13376  nninfsel  13388  nninffeq  13391  isomninnlem  13400  cvgcmp2nlemabs  13402  trilpolemlt1  13409  trirec0xor  13413  ismkvnnlem  13419