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 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 2213

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

This theorem is referenced by:  3eqtr3d  2272  3eqtr3rd  2273  3eqtr3a  2288  opth  4335  eusvnf  4556  f00  5537  f1imacnv  5609  foimacnv  5610  f1ococnv1  5621  funfvdm  5718  fvmptdf  5743  fndmdif  5761  funopsn  5838  acexmidlemph  6021  acexmidlemab  6022  ovmpodf  6163  fvmpopr2d  6168  oprssov  6174  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  oav2  6674  omv2  6676  fnsnsplitdc  6716  ecopovtrn  6844  ecopovtrng  6847  map0b  6899  en1  7016  ssenen  7080  fidifsnen  7100  dif1en  7111  undifdc  7159  fidcenumlemr  7197  ordiso2  7277  nninfninc  7365  nnnninfeq2  7371  nninfisollemne  7373  finomni  7382  exmidomni  7384  fodjum  7388  exmidaclem  7466  distrnqg  7650  1qec  7651  prarloclemarch2  7682  nnnq0lem1  7709  nqpnq0nq  7716  distrnq0  7722  prarloclemlt  7756  prmuloclemcalc  7828  ltaprg  7882  prplnqu  7883  recexprlem1ssl  7896  recexprlem1ssu  7897  ltmprr  7905  cauappcvgprlemopl  7909  caucvgprlemopl  7932  caucvgprprlemopl  7960  caucvgprprlemexb  7970  prsrlem1  8005  ltsosr  8027  mulgt0sr  8041  recidpipr  8119  recriota  8153  nntopi  8157  axcaucvglemres  8162  addlid  8361  readdcan  8362  muladd11r  8378  add32r  8382  cnegexlem2  8398  cnegex  8400  pncan2  8429  addsubass  8432  subadd23  8434  addsub12  8435  subid  8441  subid1  8442  npncan  8443  nppcan3  8446  subsub  8452  nppcan2  8453  nnncan2  8459  npncan3  8460  pnpcan  8461  negdi  8479  mvlraddd  8586  mvlladdd  8587  pnpncand  8597  subdi  8607  mulsub  8623  mulsub2  8624  eqord1  8706  recexap  8876  div32ap  8915  divsubdirap  8931  divmuldivap  8935  divdivdivap  8936  divmuleqap  8940  divcanap6  8942  dmdcanap  8945  divsubdivap  8951  div2negap  8958  div2subap  9060  mvllmulapd  9065  prodgt0gt0  9074  cju  9184  zneo  9624  infrenegsupex  9871  qreccl  9919  mul2lt0rlt0  10037  xnpcan  10150  fzosn  10494  modqid  10655  modqm1p1mod0  10681  modqltm1p1mod  10682  modqmul1  10683  modaddmodup  10693  modaddmodlo  10694  modqsubdir  10699  iseqf1olemkle  10803  iseqf1olemklt  10804  seq3f1olemstep  10820  seq3f1oleml  10822  seqf1oglem2  10826  seqfeq3  10835  seq3distr  10838  expineg2  10854  expm1t  10873  expadd  10887  expaddzaplem  10888  expmulzap  10891  sqsubswap  10905  subsq2  10953  binom2sub  10959  binom3  10963  facndiv  11045  bcval5  11069  bcn2p1  11076  bcnm1  11078  pfxccatpfx2  11365  2shfti  11452  shftcan2  11456  reim0  11482  imval2  11515  cjreim2  11525  cjdivap  11530  cnrecnv  11531  rennim  11623  resqrexlemnm  11639  remsqsqrt  11653  sqrtdiv  11663  sqrtmsq  11666  sqabsadd  11676  sqabssub  11677  absreim  11689  absdivap  11691  absnid  11694  sqabs  11703  abslt  11709  absle  11710  recvalap  11718  abssub  11722  maxabslemlub  11828  infxrnegsupex  11884  mulcn2  11933  reccn2ap  11934  cjcn2  11937  summodclem3  12002  summodclem2a  12003  summodc  12005  zsumdc  12006  fsum3  12009  fisumss  12014  fsumcl2lem  12020  fsumm1  12038  fsum1p  12040  isummulc2  12048  telfsumo  12088  binomlem  12105  bcxmas  12111  arisum  12120  trireciplem  12122  trirecip  12123  geolim2  12134  georeclim  12135  cvgratnnlemfm  12151  cvgratz  12154  mertenslemi1  12157  clim2divap  12162  prodmodclem3  12197  prodmodclem2a  12198  zproddc  12201  fprodseq  12205  fprodssdc  12212  fprod1p  12221  efcan  12298  efexp  12304  efzval  12305  efgt0  12306  eftlub  12312  efltim  12320  resinval  12337  recosval  12338  cosmul  12367  cos2t  12372  cos2tsin  12373  cos01bnd  12380  cos12dec  12390  eirraplem  12399  muldvds1  12438  dvdsexp  12483  oexpneg  12499  divalglemqt  12541  divalglemeunn  12543  divalglemeuneg  12545  divalgmod  12549  flodddiv4t2lthalf  12561  bitsmod  12578  bitsinv1lem  12583  gcdid0  12612  gcdaddm  12616  dvdsgcdidd  12626  rpmulgcd  12658  sqgcd  12661  algcvg  12681  eucalgcvga  12691  eucalg  12692  dvdslcm  12702  lcmeq0  12704  lcmgcd  12711  qredeu  12730  sqnprm  12769  divgcdodd  12776  sqrt2irrlem  12794  sqpweven  12808  2sqpwodd  12809  divnumden  12829  hashdvds  12854  phimullem  12858  eulerthlemrprm  12862  eulerthlemth  12865  odzdvds  12879  pythagtriplem3  12901  pythagtriplem4  12902  pythagtriplem14  12911  pythagtriplem19  12916  pcpremul  12927  pceulem  12928  pcqdiv  12941  pcaddlem  12973  fldivp1  12982  1arithlem4  13000  4sqlem10  13021  mul4sqlem  13027  4sqlem11  13035  4sqlem15  13039  4sqlem16  13040  4sqlem17  13041  ennnfonelemhf1o  13095  strslssd  13190  ressbas2d  13212  ressinbasd  13218  topnidg  13396  lidrideqd  13525  grpidd  13527  grprida  13531  gsumress  13539  ismndd  13581  grpidd2  13685  grpinvid1  13696  grpinvid2  13697  grppnpcan2  13738  grpnpncan  13739  dfgrp3mlem  13742  grpsubpropd2  13749  mhmid  13763  mhmmnd  13764  mulgsubcl  13784  mulgneg  13788  mulgaddcomlem  13793  mulginvinv  13796  mulgdirlem  13801  mulgdir  13802  mulgass  13807  mulgmodid  13809  grpissubg  13842  eqgcpbl  13876  ghmid  13897  ghmmulg  13904  resghm  13908  invghm  13977  gsumfzmptfidmadd  13987  mgptopng  14004  srgisid  14061  ringidss  14104  ringcom  14106  opprsubgg  14159  unitgrp  14192  1rinv  14204  0unit  14205  rhmdvdsr  14251  lringuplu  14272  subrngpropd  14292  subrgpropd  14329  lmod0vs  14397  lmodvsmmulgdi  14399  lmodvneg1  14406  lmodcom  14409  lmodsubvs  14419  lmodsubdir  14421  lmodpropd  14425  lspsnsub  14497  lspsneq0b  14503  lsppropd  14508  rlmscabas  14536  lidlbas  14554  zringmulg  14674  restopnb  14972  txcnmpt  15064  cnmpt1t  15076  blhalf  15199  xmspropd  15268  mspropd  15269  mpomulcn  15357  ivthreinc  15436  limcimolemlt  15455  dvfre  15501  dveflem  15517  dvef  15518  ply1termlem  15533  plymullem1  15539  sin2kpi  15602  cos2kpi  15603  sin2pim  15604  cos2pim  15605  ptolemy  15615  sincosq2sgn  15618  sincosq3sgn  15619  sincosq4sgn  15620  sinq12gt0  15621  tangtx  15629  sincosq1eq  15630  abssinper  15637  sinkpi  15638  relogeftb  15656  relogoprlem  15659  relogexp  15663  pellexlem1  15771  mpodvdsmulf1o  15784  mersenne  15791  perfectlem1  15793  perfectlem2  15794  perfect  15795  lgsval2lem  15809  lgsdir2lem4  15830  lgsdirprm  15833  lgsdilem2  15835  gausslemma2dlem7  15867  lgseisenlem4  15872  lgsquadlem1  15876  lgsquadlem2  15877  lgsquad2lem1  15880  lgsquad2lem2  15881  2sqlem4  15917  2sqlem6  15919  2sqlem8  15922  clwwlknonel  16353  eupth2fi  16400  peano3nninf  16713  nninfsel  16723  nninffeq  16726  isomninnlem  16742  cvgcmp2nlemabs  16744  trilpolemlt1  16753  trirec0xor  16757  qdiff  16761  ismkvnnlem  16765  gfsum0  16791