Theorem eqtr3d 2273

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3d  2279  3eqtr3rd  2280  3eqtr3a  2295  opth  4379  eusvnf  4601  f00  5587  f1imacnv  5659  foimacnv  5660  f1ococnv1  5671  funfvdm  5769  fvmptdf  5796  fndmdif  5817  funopsn  5894  acexmidlemph  6081  acexmidlemab  6082  ovmpodf  6223  fvmpopr2d  6228  oprssov  6234  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  oav2  6740  omv2  6742  fnsnsplitdc  6782  ecopovtrn  6910  ecopovtrng  6913  map0b  6972  en1  7091  ssenen  7157  fidifsnen  7177  dif1en  7188  undifdc  7236  fidcenumlemr  7278  ordiso2  7382  nninfninc  7470  nnnninfeq2  7476  nninfisollemne  7478  finomni  7487  exmidomni  7489  fodjum  7493  exmidaclem  7571  distrnqg  7761  1qec  7762  prarloclemarch2  7793  nnnq0lem1  7820  nqpnq0nq  7827  distrnq0  7833  prarloclemlt  7867  prmuloclemcalc  7939  ltaprg  7993  prplnqu  7994  recexprlem1ssl  8007  recexprlem1ssu  8008  ltmprr  8016  cauappcvgprlemopl  8020  caucvgprlemopl  8043  caucvgprprlemopl  8071  caucvgprprlemexb  8081  prsrlem1  8116  ltsosr  8138  mulgt0sr  8152  recidpipr  8230  recriota  8264  nntopi  8268  axcaucvglemres  8273  addlid  8473  readdcan  8474  muladd11r  8490  add32r  8494  cnegexlem2  8510  cnegex  8512  pncan2  8541  addsubass  8544  subadd23  8546  addsub12  8547  subid  8553  subid1  8554  npncan  8555  nppcan3  8558  subsub  8564  nppcan2  8565  nnncan2  8571  npncan3  8572  pnpcan  8573  negdi  8591  mvlraddd  8698  mvlladdd  8699  pnpncand  8709  subdi  8720  mulsub  8736  mulsub2  8737  eqord1  8819  recexap  8990  div32ap  9031  divsubdirap  9047  divmuldivap  9051  divdivdivap  9052  divmuleqap  9056  divcanap6  9058  dmdcanap  9061  divsubdivap  9067  div2negap  9074  div2subap  9176  mvllmulapd  9181  prodgt0gt0  9190  cju  9300  zneo  9759  infrenegsupex  10011  qreccl  10059  mul2lt0rlt0  10178  xnpcan  10292  fzosn  10641  modqid  10808  modqm1p1mod0  10834  modqltm1p1mod  10835  modqmul1  10836  modaddmodup  10846  modaddmodlo  10847  modqsubdir  10852  iseqf1olemkle  10956  iseqf1olemklt  10957  seq3f1olemstep  10973  seq3f1oleml  10975  seqf1oglem2  10979  seqfeq3  10988  seq3distr  10991  expineg2  11007  expm1t  11026  expadd  11040  expaddzaplem  11041  expmulzap  11044  sqsubswap  11058  subsq2  11106  binom2sub  11112  binom3  11116  resq01  11117  facndiv  11200  bcval5  11224  bcn2p1  11232  bcnm1  11234  hashpwfi  11292  hashfibclem  11305  pfxccatpfx2  11532  2shfti  11619  shftcan2  11623  reim0  11649  imval2  11682  cjreim2  11693  cjdivap  11698  cnrecnv  11699  rennim  11791  resqrexlemnm  11807  remsqsqrt  11821  sqrtdiv  11831  sqrtmsq  11834  sqabsadd  11844  sqabssub  11845  absreim  11857  absdivap  11859  absnid  11862  sqabs  11872  abslt  11878  absle  11879  recvalap  11887  abssub  11891  maxabslemlub  11997  infxrnegsupex  12055  mulcn2  12104  reccn2ap  12105  cjcn2  12108  summodclem3  12173  summodclem2a  12174  summodc  12176  zsumdc  12177  fsum3  12180  fisumss  12185  fsumcl2lem  12191  fsumm1  12209  fsum1p  12211  isummulc2  12219  telfsumo  12259  binomlem  12276  bcxmas  12282  arisum  12291  trireciplem  12293  trirecip  12294  geolim2  12305  georeclim  12306  cvgratnnlemfm  12322  cvgratz  12325  mertenslemi1  12328  clim2divap  12333  prodmodclem3  12368  prodmodclem2a  12369  zproddc  12372  fprodseq  12376  fprodssdc  12383  fprod1p  12392  efcan  12469  efexp  12475  efzval  12476  efgt0  12477  eftlub  12483  efltim  12491  resinval  12508  recosval  12509  cosmul  12538  cos2t  12543  cos2tsin  12544  cos01bnd  12551  cos12dec  12561  eirraplem  12570  muldvds1  12609  dvdsexp  12654  oexpneg  12670  divalglemqt  12712  divalglemeunn  12714  divalglemeuneg  12716  divalgmod  12720  flodddiv4t2lthalf  12732  bitsmod  12749  bitsinv1lem  12754  gcdid0  12783  gcdaddm  12787  dvdsgcdidd  12797  rpmulgcd  12829  sqgcd  12832  algcvg  12852  eucalgcvga  12862  eucalg  12863  dvdslcm  12873  lcmeq0  12875  lcmgcd  12882  qredeu  12901  sqnprm  12941  divgcdodd  12948  sqrt2irrlem  12966  sqpweven  12981  2sqpwodd  12982  divnumden  13002  hashdvds  13029  phimullem  13033  eulerthlemrprm  13037  eulerthlemth  13040  odzdvds  13054  pythagtriplem3  13076  pythagtriplem4  13077  pythagtriplem14  13086  pythagtriplem19  13091  pcpremul  13102  pceulem  13103  pcqdiv  13116  pcaddlem  13148  fldivp1  13157  1arithlem4  13175  4sqlem10  13196  mul4sqlem  13202  4sqlem11  13210  4sqlem15  13214  4sqlem16  13215  4sqlem17  13216  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemic  13309  ballotfilem1c  13310  ballotfilemfrceq  13331  ballotfilemrinv0  13335  ennnfonelemhf1o  13363  strslssd  13458  ressbas2d  13482  ressinbasd  13488  topnidg  13666  lidrideqd  13761  grpidd  13763  grprida  13767  gzsumress  13772  ismndd  13810  grpidd2  13906  grpinvid1  13917  grpinvid2  13918  grppnpcan2  13959  grpnpncan  13960  dfgrp3mlem  13963  grpsubpropd2  13970  mhmid  13978  mhmmnd  13979  mulgsubcl  13999  mulgneg  14003  mulgaddcomlem  14008  mulginvinv  14011  mulgdirlem  14016  mulgdir  14017  mulgass  14022  mulgmodid  14024  grpissubg  14057  eqgcpbl  14091  ghmid  14112  ghmmulg  14119  resghm  14123  cntrsubgnsg  14176  invghm  14224  gsum0cmn  14245  gsumresfi  14264  gsum2dfilem2  14273  mgptopng  14336  srgisid  14398  ringidss  14442  ringcom  14444  opprsubgg  14500  unitgrp  14533  1rinv  14545  0unit  14546  rhmdvdsr  14592  lringuplu  14613  subrngpropd  14634  subrgpropd  14671  lmod0vs  14768  lmodvsmmulgdi  14770  lmodvneg1  14777  lmodcom  14780  lmodsubvs  14790  lmodsubdir  14792  lmodpropd  14796  lspsnsub  14868  lspsneq0b  14874  lsppropd  14879  rlmscabas  14907  lidlbas  14925  zringmulg  15043  restopnb  15419  txcnmpt  15511  cnmpt1t  15523  blhalf  15646  xmspropd  15715  mspropd  15716  mpomulcn  15804  ivthreinc  15883  limcimolemlt  15902  dvfre  15948  dveflem  15964  dvef  15965  ply1termlem  15980  plymullem1  15986  sin2kpi  16050  cos2kpi  16051  sin2pim  16052  cos2pim  16053  ptolemy  16063  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  tangtx  16077  sincosq1eq  16078  abssinper  16085  sinkpi  16086  sineq0re  16088  root1idef  16096  relogeftb  16106  relogoprlem  16110  relogexp  16114  rpcxpmul2z  16160  log2tlbndlog2  16232  birthdaylem2  16238  birthdaylem3  16239  pellexlem1  16241  efchtqdvds  16277  ppiqp1le  16279  ppiqltx  16293  mpodvdsmulf1o  16296  ppiqub  16305  chtqub  16308  mersenne  16309  perfectlem1  16311  perfectlem2  16312  perfect  16313  bposlem6  16328  bposlem9  16331  lgsval2lem  16346  lgsdir2lem4  16367  lgsdirprm  16370  lgsdilem2  16372  gausslemma2dlem7  16404  lgseisenlem4  16409  lgsquadlem1  16413  lgsquadlem2  16414  lgsquad2lem1  16417  lgsquad2lem2  16418  2sqlem4  16454  2sqlem6  16456  2sqlem8  16459  clwwlknonel  16890  eupth2fi  16937  dichmul0orlem2  16971  dichmul0orlem3  16972  dichmul0orlem4  16973  peano3nninf  17268  nninfsel  17278  nninffeq  17281  isomninnlem  17297  cvgcmp2nlemabs  17299  trilpolemlt1  17309  trirec0xor  17313  qdiff  17317  ismkvnnlem  17321