Theorem eqtr3d 2269

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 2240	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqtr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtrd 2267	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  3eqtr3d  2275  3eqtr3rd  2276  3eqtr3a  2291  opth  4358  eusvnf  4579  f00  5564  f1imacnv  5636  foimacnv  5637  f1ococnv1  5648  funfvdm  5745  fvmptdf  5770  fndmdif  5788  funopsn  5865  acexmidlemph  6051  acexmidlemab  6052  ovmpodf  6193  fvmpopr2d  6198  oprssov  6204  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  oav2  6709  omv2  6711  fnsnsplitdc  6751  ecopovtrn  6879  ecopovtrng  6882  map0b  6934  en1  7052  ssenen  7118  fidifsnen  7138  dif1en  7149  undifdc  7197  fidcenumlemr  7238  ordiso2  7339  nninfninc  7427  nnnninfeq2  7433  nninfisollemne  7435  finomni  7444  exmidomni  7446  fodjum  7450  exmidaclem  7528  distrnqg  7718  1qec  7719  prarloclemarch2  7750  nnnq0lem1  7777  nqpnq0nq  7784  distrnq0  7790  prarloclemlt  7824  prmuloclemcalc  7896  ltaprg  7950  prplnqu  7951  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  cauappcvgprlemopl  7977  caucvgprlemopl  8000  caucvgprprlemopl  8028  caucvgprprlemexb  8038  prsrlem1  8073  ltsosr  8095  mulgt0sr  8109  recidpipr  8187  recriota  8221  nntopi  8225  axcaucvglemres  8230  addlid  8428  readdcan  8429  muladd11r  8445  add32r  8449  cnegexlem2  8465  cnegex  8467  pncan2  8496  addsubass  8499  subadd23  8501  addsub12  8502  subid  8508  subid1  8509  npncan  8510  nppcan3  8513  subsub  8519  nppcan2  8520  nnncan2  8526  npncan3  8527  pnpcan  8528  negdi  8546  mvlraddd  8653  mvlladdd  8654  pnpncand  8664  subdi  8675  mulsub  8691  mulsub2  8692  eqord1  8774  recexap  8944  div32ap  8983  divsubdirap  8999  divmuldivap  9003  divdivdivap  9004  divmuleqap  9008  divcanap6  9010  dmdcanap  9013  divsubdivap  9019  div2negap  9026  div2subap  9128  mvllmulapd  9133  prodgt0gt0  9142  cju  9252  zneo  9697  infrenegsupex  9944  qreccl  9992  mul2lt0rlt0  10110  xnpcan  10224  fzosn  10572  modqid  10735  modqm1p1mod0  10761  modqltm1p1mod  10762  modqmul1  10763  modaddmodup  10773  modaddmodlo  10774  modqsubdir  10779  iseqf1olemkle  10883  iseqf1olemklt  10884  seq3f1olemstep  10900  seq3f1oleml  10902  seqf1oglem2  10906  seqfeq3  10915  seq3distr  10918  expineg2  10934  expm1t  10953  expadd  10967  expaddzaplem  10968  expmulzap  10971  sqsubswap  10985  subsq2  11033  binom2sub  11039  binom3  11043  resq01  11044  facndiv  11126  bcval5  11150  bcn2p1  11158  bcnm1  11160  hashpwfi  11218  hashfibclem  11231  pfxccatpfx2  11454  2shfti  11541  shftcan2  11545  reim0  11571  imval2  11604  cjreim2  11614  cjdivap  11619  cnrecnv  11620  rennim  11712  resqrexlemnm  11728  remsqsqrt  11742  sqrtdiv  11752  sqrtmsq  11755  sqabsadd  11765  sqabssub  11766  absreim  11778  absdivap  11780  absnid  11783  sqabs  11792  abslt  11798  absle  11799  recvalap  11807  abssub  11811  maxabslemlub  11917  infxrnegsupex  11973  mulcn2  12022  reccn2ap  12023  cjcn2  12026  summodclem3  12091  summodclem2a  12092  summodc  12094  zsumdc  12095  fsum3  12098  fisumss  12103  fsumcl2lem  12109  fsumm1  12127  fsum1p  12129  isummulc2  12137  telfsumo  12177  binomlem  12194  bcxmas  12200  arisum  12209  trireciplem  12211  trirecip  12212  geolim2  12223  georeclim  12224  cvgratnnlemfm  12240  cvgratz  12243  mertenslemi1  12246  clim2divap  12251  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodssdc  12301  fprod1p  12310  efcan  12387  efexp  12393  efzval  12394  efgt0  12395  eftlub  12401  efltim  12409  resinval  12426  recosval  12427  cosmul  12456  cos2t  12461  cos2tsin  12462  cos01bnd  12469  cos12dec  12479  eirraplem  12488  muldvds1  12527  dvdsexp  12572  oexpneg  12588  divalglemqt  12630  divalglemeunn  12632  divalglemeuneg  12634  divalgmod  12638  flodddiv4t2lthalf  12650  bitsmod  12667  bitsinv1lem  12672  gcdid0  12701  gcdaddm  12705  dvdsgcdidd  12715  rpmulgcd  12747  sqgcd  12750  algcvg  12770  eucalgcvga  12780  eucalg  12781  dvdslcm  12791  lcmeq0  12793  lcmgcd  12800  qredeu  12819  sqnprm  12858  divgcdodd  12865  sqrt2irrlem  12883  sqpweven  12897  2sqpwodd  12898  divnumden  12918  hashdvds  12943  phimullem  12947  eulerthlemrprm  12951  eulerthlemth  12954  odzdvds  12968  pythagtriplem3  12990  pythagtriplem4  12991  pythagtriplem14  13000  pythagtriplem19  13005  pcpremul  13016  pceulem  13017  pcqdiv  13030  pcaddlem  13062  fldivp1  13071  1arithlem4  13089  4sqlem10  13110  mul4sqlem  13116  4sqlem11  13124  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemfrceq  13216  ballotfilemrinv0  13220  ennnfonelemhf1o  13248  strslssd  13343  ressbas2d  13365  ressinbasd  13371  topnidg  13549  lidrideqd  13678  grpidd  13680  grprida  13684  gsumress  13692  ismndd  13734  grpidd2  13838  grpinvid1  13849  grpinvid2  13850  grppnpcan2  13891  grpnpncan  13892  dfgrp3mlem  13895  grpsubpropd2  13902  mhmid  13916  mhmmnd  13917  mulgsubcl  13937  mulgneg  13941  mulgaddcomlem  13946  mulginvinv  13949  mulgdirlem  13954  mulgdir  13955  mulgass  13960  mulgmodid  13962  grpissubg  13995  eqgcpbl  14029  ghmid  14050  ghmmulg  14057  resghm  14061  invghm  14130  gsumfzmptfidmadd  14140  mgptopng  14157  srgisid  14214  ringidss  14257  ringcom  14259  opprsubgg  14313  unitgrp  14346  1rinv  14358  0unit  14359  rhmdvdsr  14405  lringuplu  14426  subrngpropd  14447  subrgpropd  14484  lmod0vs  14581  lmodvsmmulgdi  14583  lmodvneg1  14590  lmodcom  14593  lmodsubvs  14603  lmodsubdir  14605  lmodpropd  14609  lspsnsub  14681  lspsneq0b  14687  lsppropd  14692  rlmscabas  14720  lidlbas  14738  zringmulg  14858  restopnb  15158  txcnmpt  15250  cnmpt1t  15262  blhalf  15385  xmspropd  15454  mspropd  15455  mpomulcn  15543  ivthreinc  15622  limcimolemlt  15641  dvfre  15687  dveflem  15703  dvef  15704  ply1termlem  15719  plymullem1  15725  sin2kpi  15788  cos2kpi  15789  sin2pim  15790  cos2pim  15791  ptolemy  15801  sincosq2sgn  15804  sincosq3sgn  15805  sincosq4sgn  15806  sinq12gt0  15807  tangtx  15815  sincosq1eq  15816  abssinper  15823  sinkpi  15824  relogeftb  15842  relogoprlem  15845  relogexp  15849  pellexlem1  15957  mpodvdsmulf1o  15970  mersenne  15977  perfectlem1  15979  perfectlem2  15980  perfect  15981  lgsval2lem  15995  lgsdir2lem4  16016  lgsdirprm  16019  lgsdilem2  16021  gausslemma2dlem7  16053  lgseisenlem4  16058  lgsquadlem1  16062  lgsquadlem2  16063  lgsquad2lem1  16066  lgsquad2lem2  16067  2sqlem4  16103  2sqlem6  16105  2sqlem8  16108  clwwlknonel  16539  eupth2fi  16586  peano3nninf  16897  nninfsel  16907  nninffeq  16910  isomninnlem  16926  cvgcmp2nlemabs  16928  trilpolemlt1  16937  trirec0xor  16941  qdiff  16945  ismkvnnlem  16949  gfsum0  16976