Theorem eqtr3d 2267

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

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

This theorem is referenced by:  3eqtr3d  2273  3eqtr3rd  2274  3eqtr3a  2289  opth  4352  eusvnf  4573  f00  5558  f1imacnv  5630  foimacnv  5631  f1ococnv1  5642  funfvdm  5739  fvmptdf  5764  fndmdif  5782  funopsn  5859  acexmidlemph  6042  acexmidlemab  6043  ovmpodf  6184  fvmpopr2d  6189  oprssov  6195  tfrlemisucaccv  6555  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  oav2  6695  omv2  6697  fnsnsplitdc  6737  ecopovtrn  6865  ecopovtrng  6868  map0b  6920  en1  7038  ssenen  7104  fidifsnen  7124  dif1en  7135  undifdc  7183  fidcenumlemr  7224  ordiso2  7325  nninfninc  7413  nnnninfeq2  7419  nninfisollemne  7421  finomni  7430  exmidomni  7432  fodjum  7436  exmidaclem  7514  distrnqg  7701  1qec  7702  prarloclemarch2  7733  nnnq0lem1  7760  nqpnq0nq  7767  distrnq0  7773  prarloclemlt  7807  prmuloclemcalc  7879  ltaprg  7933  prplnqu  7934  recexprlem1ssl  7947  recexprlem1ssu  7948  ltmprr  7956  cauappcvgprlemopl  7960  caucvgprlemopl  7983  caucvgprprlemopl  8011  caucvgprprlemexb  8021  prsrlem1  8056  ltsosr  8078  mulgt0sr  8092  recidpipr  8170  recriota  8204  nntopi  8208  axcaucvglemres  8213  addlid  8411  readdcan  8412  muladd11r  8428  add32r  8432  cnegexlem2  8448  cnegex  8450  pncan2  8479  addsubass  8482  subadd23  8484  addsub12  8485  subid  8491  subid1  8492  npncan  8493  nppcan3  8496  subsub  8502  nppcan2  8503  nnncan2  8509  npncan3  8510  pnpcan  8511  negdi  8529  mvlraddd  8636  mvlladdd  8637  pnpncand  8647  subdi  8657  mulsub  8673  mulsub2  8674  eqord1  8756  recexap  8926  div32ap  8965  divsubdirap  8981  divmuldivap  8985  divdivdivap  8986  divmuleqap  8990  divcanap6  8992  dmdcanap  8995  divsubdivap  9001  div2negap  9008  div2subap  9110  mvllmulapd  9115  prodgt0gt0  9124  cju  9234  zneo  9678  infrenegsupex  9925  qreccl  9973  mul2lt0rlt0  10091  xnpcan  10204  fzosn  10549  modqid  10710  modqm1p1mod0  10736  modqltm1p1mod  10737  modqmul1  10738  modaddmodup  10748  modaddmodlo  10749  modqsubdir  10754  iseqf1olemkle  10858  iseqf1olemklt  10859  seq3f1olemstep  10875  seq3f1oleml  10877  seqf1oglem2  10881  seqfeq3  10890  seq3distr  10893  expineg2  10909  expm1t  10928  expadd  10942  expaddzaplem  10943  expmulzap  10946  sqsubswap  10960  subsq2  11008  binom2sub  11014  binom3  11018  facndiv  11100  bcval5  11124  bcn2p1  11131  bcnm1  11133  hashfibclem  11202  pfxccatpfx2  11425  2shfti  11512  shftcan2  11516  reim0  11542  imval2  11575  cjreim2  11585  cjdivap  11590  cnrecnv  11591  rennim  11683  resqrexlemnm  11699  remsqsqrt  11713  sqrtdiv  11723  sqrtmsq  11726  sqabsadd  11736  sqabssub  11737  absreim  11749  absdivap  11751  absnid  11754  sqabs  11763  abslt  11769  absle  11770  recvalap  11778  abssub  11782  maxabslemlub  11888  infxrnegsupex  11944  mulcn2  11993  reccn2ap  11994  cjcn2  11997  summodclem3  12062  summodclem2a  12063  summodc  12065  zsumdc  12066  fsum3  12069  fisumss  12074  fsumcl2lem  12080  fsumm1  12098  fsum1p  12100  isummulc2  12108  telfsumo  12148  binomlem  12165  bcxmas  12171  arisum  12180  trireciplem  12182  trirecip  12183  geolim2  12194  georeclim  12195  cvgratnnlemfm  12211  cvgratz  12214  mertenslemi1  12217  clim2divap  12222  prodmodclem3  12257  prodmodclem2a  12258  zproddc  12261  fprodseq  12265  fprodssdc  12272  fprod1p  12281  efcan  12358  efexp  12364  efzval  12365  efgt0  12366  eftlub  12372  efltim  12380  resinval  12397  recosval  12398  cosmul  12427  cos2t  12432  cos2tsin  12433  cos01bnd  12440  cos12dec  12450  eirraplem  12459  muldvds1  12498  dvdsexp  12543  oexpneg  12559  divalglemqt  12601  divalglemeunn  12603  divalglemeuneg  12605  divalgmod  12609  flodddiv4t2lthalf  12621  bitsmod  12638  bitsinv1lem  12643  gcdid0  12672  gcdaddm  12676  dvdsgcdidd  12686  rpmulgcd  12718  sqgcd  12721  algcvg  12741  eucalgcvga  12751  eucalg  12752  dvdslcm  12762  lcmeq0  12764  lcmgcd  12771  qredeu  12790  sqnprm  12829  divgcdodd  12836  sqrt2irrlem  12854  sqpweven  12868  2sqpwodd  12869  divnumden  12889  hashdvds  12914  phimullem  12918  eulerthlemrprm  12922  eulerthlemth  12925  odzdvds  12939  pythagtriplem3  12961  pythagtriplem4  12962  pythagtriplem14  12971  pythagtriplem19  12976  pcpremul  12987  pceulem  12988  pcqdiv  13001  pcaddlem  13033  fldivp1  13042  1arithlem4  13060  4sqlem10  13081  mul4sqlem  13087  4sqlem11  13095  4sqlem15  13099  4sqlem16  13100  4sqlem17  13101  ennnfonelemhf1o  13156  strslssd  13251  ressbas2d  13273  ressinbasd  13279  topnidg  13457  lidrideqd  13586  grpidd  13588  grprida  13592  gsumress  13600  ismndd  13642  grpidd2  13746  grpinvid1  13757  grpinvid2  13758  grppnpcan2  13799  grpnpncan  13800  dfgrp3mlem  13803  grpsubpropd2  13810  mhmid  13824  mhmmnd  13825  mulgsubcl  13845  mulgneg  13849  mulgaddcomlem  13854  mulginvinv  13857  mulgdirlem  13862  mulgdir  13863  mulgass  13868  mulgmodid  13870  grpissubg  13903  eqgcpbl  13937  ghmid  13958  ghmmulg  13965  resghm  13969  invghm  14038  gsumfzmptfidmadd  14048  mgptopng  14065  srgisid  14122  ringidss  14165  ringcom  14167  opprsubgg  14220  unitgrp  14253  1rinv  14265  0unit  14266  rhmdvdsr  14312  lringuplu  14333  subrngpropd  14353  subrgpropd  14390  lmod0vs  14461  lmodvsmmulgdi  14463  lmodvneg1  14470  lmodcom  14473  lmodsubvs  14483  lmodsubdir  14485  lmodpropd  14489  lspsnsub  14561  lspsneq0b  14567  lsppropd  14572  rlmscabas  14600  lidlbas  14618  zringmulg  14738  restopnb  15038  txcnmpt  15130  cnmpt1t  15142  blhalf  15265  xmspropd  15334  mspropd  15335  mpomulcn  15423  ivthreinc  15502  limcimolemlt  15521  dvfre  15567  dveflem  15583  dvef  15584  ply1termlem  15599  plymullem1  15605  sin2kpi  15668  cos2kpi  15669  sin2pim  15670  cos2pim  15671  ptolemy  15681  sincosq2sgn  15684  sincosq3sgn  15685  sincosq4sgn  15686  sinq12gt0  15687  tangtx  15695  sincosq1eq  15696  abssinper  15703  sinkpi  15704  relogeftb  15722  relogoprlem  15725  relogexp  15729  pellexlem1  15837  mpodvdsmulf1o  15850  mersenne  15857  perfectlem1  15859  perfectlem2  15860  perfect  15861  lgsval2lem  15875  lgsdir2lem4  15896  lgsdirprm  15899  lgsdilem2  15901  gausslemma2dlem7  15933  lgseisenlem4  15938  lgsquadlem1  15942  lgsquadlem2  15943  lgsquad2lem1  15946  lgsquad2lem2  15947  2sqlem4  15983  2sqlem6  15985  2sqlem8  15988  clwwlknonel  16419  eupth2fi  16466  peano3nninf  16777  nninfsel  16787  nninffeq  16790  isomninnlem  16806  cvgcmp2nlemabs  16808  trilpolemlt1  16817  trirec0xor  16821  qdiff  16825  ismkvnnlem  16829  gfsum0  16855