Theorem eqtr3d 2266

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr3d  2272  3eqtr3rd  2273  3eqtr3a  2288  opth  4329  eusvnf  4550  f00  5528  f1imacnv  5600  foimacnv  5601  f1ococnv1  5612  funfvdm  5709  fvmptdf  5734  fndmdif  5752  funopsn  5830  acexmidlemph  6011  acexmidlemab  6012  ovmpodf  6153  fvmpopr2d  6158  oprssov  6164  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  oav2  6631  omv2  6633  fnsnsplitdc  6673  ecopovtrn  6801  ecopovtrng  6804  map0b  6856  en1  6973  ssenen  7037  fidifsnen  7057  dif1en  7068  undifdc  7116  fidcenumlemr  7154  ordiso2  7234  nninfninc  7322  nnnninfeq2  7328  nninfisollemne  7330  finomni  7339  exmidomni  7341  fodjum  7345  exmidaclem  7423  distrnqg  7607  1qec  7608  prarloclemarch2  7639  nnnq0lem1  7666  nqpnq0nq  7673  distrnq0  7679  prarloclemlt  7713  prmuloclemcalc  7785  ltaprg  7839  prplnqu  7840  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  cauappcvgprlemopl  7866  caucvgprlemopl  7889  caucvgprprlemopl  7917  caucvgprprlemexb  7927  prsrlem1  7962  ltsosr  7984  mulgt0sr  7998  recidpipr  8076  recriota  8110  nntopi  8114  axcaucvglemres  8119  addlid  8318  readdcan  8319  muladd11r  8335  add32r  8339  cnegexlem2  8355  cnegex  8357  pncan2  8386  addsubass  8389  subadd23  8391  addsub12  8392  subid  8398  subid1  8399  npncan  8400  nppcan3  8403  subsub  8409  nppcan2  8410  nnncan2  8416  npncan3  8417  pnpcan  8418  negdi  8436  mvlraddd  8543  mvlladdd  8544  pnpncand  8554  subdi  8564  mulsub  8580  mulsub2  8581  eqord1  8663  recexap  8833  div32ap  8872  divsubdirap  8888  divmuldivap  8892  divdivdivap  8893  divmuleqap  8897  divcanap6  8899  dmdcanap  8902  divsubdivap  8908  div2negap  8915  div2subap  9017  mvllmulapd  9022  prodgt0gt0  9031  cju  9141  zneo  9581  infrenegsupex  9828  qreccl  9876  mul2lt0rlt0  9994  xnpcan  10107  fzosn  10451  modqid  10612  modqm1p1mod0  10638  modqltm1p1mod  10639  modqmul1  10640  modaddmodup  10650  modaddmodlo  10651  modqsubdir  10656  iseqf1olemkle  10760  iseqf1olemklt  10761  seq3f1olemstep  10777  seq3f1oleml  10779  seqf1oglem2  10783  seqfeq3  10792  seq3distr  10795  expineg2  10811  expm1t  10830  expadd  10844  expaddzaplem  10845  expmulzap  10848  sqsubswap  10862  subsq2  10910  binom2sub  10916  binom3  10920  facndiv  11002  bcval5  11026  bcn2p1  11033  bcnm1  11035  pfxccatpfx2  11322  2shfti  11396  shftcan2  11400  reim0  11426  imval2  11459  cjreim2  11469  cjdivap  11474  cnrecnv  11475  rennim  11567  resqrexlemnm  11583  remsqsqrt  11597  sqrtdiv  11607  sqrtmsq  11610  sqabsadd  11620  sqabssub  11621  absreim  11633  absdivap  11635  absnid  11638  sqabs  11647  abslt  11653  absle  11654  recvalap  11662  abssub  11666  maxabslemlub  11772  infxrnegsupex  11828  mulcn2  11877  reccn2ap  11878  cjcn2  11881  summodclem3  11946  summodclem2a  11947  summodc  11949  zsumdc  11950  fsum3  11953  fisumss  11958  fsumcl2lem  11964  fsumm1  11982  fsum1p  11984  isummulc2  11992  telfsumo  12032  binomlem  12049  bcxmas  12055  arisum  12064  trireciplem  12066  trirecip  12067  geolim2  12078  georeclim  12079  cvgratnnlemfm  12095  cvgratz  12098  mertenslemi1  12101  clim2divap  12106  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  fprodssdc  12156  fprod1p  12165  efcan  12242  efexp  12248  efzval  12249  efgt0  12250  eftlub  12256  efltim  12264  resinval  12281  recosval  12282  cosmul  12311  cos2t  12316  cos2tsin  12317  cos01bnd  12324  cos12dec  12334  eirraplem  12343  muldvds1  12382  dvdsexp  12427  oexpneg  12443  divalglemqt  12485  divalglemeunn  12487  divalglemeuneg  12489  divalgmod  12493  flodddiv4t2lthalf  12505  bitsmod  12522  bitsinv1lem  12527  gcdid0  12556  gcdaddm  12560  dvdsgcdidd  12570  rpmulgcd  12602  sqgcd  12605  algcvg  12625  eucalgcvga  12635  eucalg  12636  dvdslcm  12646  lcmeq0  12648  lcmgcd  12655  qredeu  12674  sqnprm  12713  divgcdodd  12720  sqrt2irrlem  12738  sqpweven  12752  2sqpwodd  12753  divnumden  12773  hashdvds  12798  phimullem  12802  eulerthlemrprm  12806  eulerthlemth  12809  odzdvds  12823  pythagtriplem3  12845  pythagtriplem4  12846  pythagtriplem14  12855  pythagtriplem19  12860  pcpremul  12871  pceulem  12872  pcqdiv  12885  pcaddlem  12917  fldivp1  12926  1arithlem4  12944  4sqlem10  12965  mul4sqlem  12971  4sqlem11  12979  4sqlem15  12983  4sqlem16  12984  4sqlem17  12985  ennnfonelemhf1o  13039  strslssd  13134  ressbas2d  13156  ressinbasd  13162  topnidg  13340  lidrideqd  13469  grpidd  13471  grprida  13475  gsumress  13483  ismndd  13525  grpidd2  13629  grpinvid1  13640  grpinvid2  13641  grppnpcan2  13682  grpnpncan  13683  dfgrp3mlem  13686  grpsubpropd2  13693  mhmid  13707  mhmmnd  13708  mulgsubcl  13728  mulgneg  13732  mulgaddcomlem  13737  mulginvinv  13740  mulgdirlem  13745  mulgdir  13746  mulgass  13751  mulgmodid  13753  grpissubg  13786  eqgcpbl  13820  ghmid  13841  ghmmulg  13848  resghm  13852  invghm  13921  gsumfzmptfidmadd  13931  mgptopng  13948  srgisid  14005  ringidss  14048  ringcom  14050  opprsubgg  14103  unitgrp  14136  1rinv  14148  0unit  14149  rhmdvdsr  14195  lringuplu  14216  subrngpropd  14236  subrgpropd  14273  lmod0vs  14341  lmodvsmmulgdi  14343  lmodvneg1  14350  lmodcom  14353  lmodsubvs  14363  lmodsubdir  14365  lmodpropd  14369  lspsnsub  14441  lspsneq0b  14447  lsppropd  14452  rlmscabas  14480  lidlbas  14498  zringmulg  14618  restopnb  14911  txcnmpt  15003  cnmpt1t  15015  blhalf  15138  xmspropd  15207  mspropd  15208  mpomulcn  15296  ivthreinc  15375  limcimolemlt  15394  dvfre  15440  dveflem  15456  dvef  15457  ply1termlem  15472  plymullem1  15478  sin2kpi  15541  cos2kpi  15542  sin2pim  15543  cos2pim  15544  ptolemy  15554  sincosq2sgn  15557  sincosq3sgn  15558  sincosq4sgn  15559  sinq12gt0  15560  tangtx  15568  sincosq1eq  15569  abssinper  15576  sinkpi  15577  relogeftb  15595  relogoprlem  15598  relogexp  15602  mpodvdsmulf1o  15720  mersenne  15727  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgsval2lem  15745  lgsdir2lem4  15766  lgsdirprm  15769  lgsdilem2  15771  gausslemma2dlem7  15803  lgseisenlem4  15808  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem1  15816  lgsquad2lem2  15817  2sqlem4  15853  2sqlem6  15855  2sqlem8  15858  clwwlknonel  16289  eupth2fi  16336  peano3nninf  16635  nninfsel  16645  nninffeq  16648  isomninnlem  16660  cvgcmp2nlemabs  16662  trilpolemlt1  16671  trirec0xor  16675  ismkvnnlem  16682  gfsum0  16708