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  11319  2shfti  11393  shftcan2  11397  reim0  11423  imval2  11456  cjreim2  11466  cjdivap  11471  cnrecnv  11472  rennim  11564  resqrexlemnm  11580  remsqsqrt  11594  sqrtdiv  11604  sqrtmsq  11607  sqabsadd  11617  sqabssub  11618  absreim  11630  absdivap  11632  absnid  11635  sqabs  11644  abslt  11650  absle  11651  recvalap  11659  abssub  11663  maxabslemlub  11769  infxrnegsupex  11825  mulcn2  11874  reccn2ap  11875  cjcn2  11878  summodclem3  11943  summodclem2a  11944  summodc  11946  zsumdc  11947  fsum3  11950  fisumss  11955  fsumcl2lem  11961  fsumm1  11979  fsum1p  11981  isummulc2  11989  telfsumo  12029  binomlem  12046  bcxmas  12052  arisum  12061  trireciplem  12063  trirecip  12064  geolim2  12075  georeclim  12076  cvgratnnlemfm  12092  cvgratz  12095  mertenslemi1  12098  clim2divap  12103  prodmodclem3  12138  prodmodclem2a  12139  zproddc  12142  fprodseq  12146  fprodssdc  12153  fprod1p  12162  efcan  12239  efexp  12245  efzval  12246  efgt0  12247  eftlub  12253  efltim  12261  resinval  12278  recosval  12279  cosmul  12308  cos2t  12313  cos2tsin  12314  cos01bnd  12321  cos12dec  12331  eirraplem  12340  muldvds1  12379  dvdsexp  12424  oexpneg  12440  divalglemqt  12482  divalglemeunn  12484  divalglemeuneg  12486  divalgmod  12490  flodddiv4t2lthalf  12502  bitsmod  12519  bitsinv1lem  12524  gcdid0  12553  gcdaddm  12557  dvdsgcdidd  12567  rpmulgcd  12599  sqgcd  12602  algcvg  12622  eucalgcvga  12632  eucalg  12633  dvdslcm  12643  lcmeq0  12645  lcmgcd  12652  qredeu  12671  sqnprm  12710  divgcdodd  12717  sqrt2irrlem  12735  sqpweven  12749  2sqpwodd  12750  divnumden  12770  hashdvds  12795  phimullem  12799  eulerthlemrprm  12803  eulerthlemth  12806  odzdvds  12820  pythagtriplem3  12842  pythagtriplem4  12843  pythagtriplem14  12852  pythagtriplem19  12857  pcpremul  12868  pceulem  12869  pcqdiv  12882  pcaddlem  12914  fldivp1  12923  1arithlem4  12941  4sqlem10  12962  mul4sqlem  12968  4sqlem11  12976  4sqlem15  12980  4sqlem16  12981  4sqlem17  12982  ennnfonelemhf1o  13036  strslssd  13131  ressbas2d  13153  ressinbasd  13159  topnidg  13337  lidrideqd  13466  grpidd  13468  grprida  13472  gsumress  13480  ismndd  13522  grpidd2  13626  grpinvid1  13637  grpinvid2  13638  grppnpcan2  13679  grpnpncan  13680  dfgrp3mlem  13683  grpsubpropd2  13690  mhmid  13704  mhmmnd  13705  mulgsubcl  13725  mulgneg  13729  mulgaddcomlem  13734  mulginvinv  13737  mulgdirlem  13742  mulgdir  13743  mulgass  13748  mulgmodid  13750  grpissubg  13783  eqgcpbl  13817  ghmid  13838  ghmmulg  13845  resghm  13849  invghm  13918  gsumfzmptfidmadd  13928  mgptopng  13945  srgisid  14002  ringidss  14045  ringcom  14047  opprsubgg  14100  unitgrp  14133  1rinv  14145  0unit  14146  rhmdvdsr  14192  lringuplu  14213  subrngpropd  14233  subrgpropd  14270  lmod0vs  14338  lmodvsmmulgdi  14340  lmodvneg1  14347  lmodcom  14350  lmodsubvs  14360  lmodsubdir  14362  lmodpropd  14366  lspsnsub  14438  lspsneq0b  14444  lsppropd  14449  rlmscabas  14477  lidlbas  14495  zringmulg  14615  restopnb  14908  txcnmpt  15000  cnmpt1t  15012  blhalf  15135  xmspropd  15204  mspropd  15205  mpomulcn  15293  ivthreinc  15372  limcimolemlt  15391  dvfre  15437  dveflem  15453  dvef  15454  ply1termlem  15469  plymullem1  15475  sin2kpi  15538  cos2kpi  15539  sin2pim  15540  cos2pim  15541  ptolemy  15551  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  sinq12gt0  15557  tangtx  15565  sincosq1eq  15566  abssinper  15573  sinkpi  15574  relogeftb  15592  relogoprlem  15595  relogexp  15599  mpodvdsmulf1o  15717  mersenne  15724  perfectlem1  15726  perfectlem2  15727  perfect  15728  lgsval2lem  15742  lgsdir2lem4  15763  lgsdirprm  15766  lgsdilem2  15768  gausslemma2dlem7  15800  lgseisenlem4  15805  lgsquadlem1  15809  lgsquadlem2  15810  lgsquad2lem1  15813  lgsquad2lem2  15814  2sqlem4  15850  2sqlem6  15852  2sqlem8  15855  clwwlknonel  16286  eupth2fi  16333  peano3nninf  16626  nninfsel  16636  nninffeq  16639  isomninnlem  16651  cvgcmp2nlemabs  16653  trilpolemlt1  16662  trirec0xor  16666  ismkvnnlem  16673  gfsum0  16699