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 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtr3d  2279  3eqtr3rd  2280  3eqtr3a  2295  opth  4375  eusvnf  4597  f00  5582  f1imacnv  5654  foimacnv  5655  f1ococnv1  5666  funfvdm  5763  fvmptdf  5790  fndmdif  5808  funopsn  5885  acexmidlemph  6072  acexmidlemab  6073  ovmpodf  6214  fvmpopr2d  6219  oprssov  6225  tfrlemisucaccv  6590  tfr1onlemsucaccv  6606  tfrcllemsucaccv  6619  oav2  6730  omv2  6732  fnsnsplitdc  6772  ecopovtrn  6900  ecopovtrng  6903  map0b  6962  en1  7080  ssenen  7146  fidifsnen  7166  dif1en  7177  undifdc  7225  fidcenumlemr  7266  ordiso2  7369  nninfninc  7457  nnnninfeq2  7463  nninfisollemne  7465  finomni  7474  exmidomni  7476  fodjum  7480  exmidaclem  7558  distrnqg  7748  1qec  7749  prarloclemarch2  7780  nnnq0lem1  7807  nqpnq0nq  7814  distrnq0  7820  prarloclemlt  7854  prmuloclemcalc  7926  ltaprg  7980  prplnqu  7981  recexprlem1ssl  7994  recexprlem1ssu  7995  ltmprr  8003  cauappcvgprlemopl  8007  caucvgprlemopl  8030  caucvgprprlemopl  8058  caucvgprprlemexb  8068  prsrlem1  8103  ltsosr  8125  mulgt0sr  8139  recidpipr  8217  recriota  8251  nntopi  8255  axcaucvglemres  8260  addlid  8459  readdcan  8460  muladd11r  8476  add32r  8480  cnegexlem2  8496  cnegex  8498  pncan2  8527  addsubass  8530  subadd23  8532  addsub12  8533  subid  8539  subid1  8540  npncan  8541  nppcan3  8544  subsub  8550  nppcan2  8551  nnncan2  8557  npncan3  8558  pnpcan  8559  negdi  8577  mvlraddd  8684  mvlladdd  8685  pnpncand  8695  subdi  8706  mulsub  8722  mulsub2  8723  eqord1  8805  recexap  8975  div32ap  9016  divsubdirap  9032  divmuldivap  9036  divdivdivap  9037  divmuleqap  9041  divcanap6  9043  dmdcanap  9046  divsubdivap  9052  div2negap  9059  div2subap  9161  mvllmulapd  9166  prodgt0gt0  9175  cju  9285  zneo  9730  infrenegsupex  9977  qreccl  10025  mul2lt0rlt0  10143  xnpcan  10257  fzosn  10606  modqid  10769  modqm1p1mod0  10795  modqltm1p1mod  10796  modqmul1  10797  modaddmodup  10807  modaddmodlo  10808  modqsubdir  10813  iseqf1olemkle  10917  iseqf1olemklt  10918  seq3f1olemstep  10934  seq3f1oleml  10936  seqf1oglem2  10940  seqfeq3  10949  seq3distr  10952  expineg2  10968  expm1t  10987  expadd  11001  expaddzaplem  11002  expmulzap  11005  sqsubswap  11019  subsq2  11067  binom2sub  11073  binom3  11077  resq01  11078  facndiv  11160  bcval5  11184  bcn2p1  11192  bcnm1  11194  hashpwfi  11252  hashfibclem  11265  pfxccatpfx2  11492  2shfti  11579  shftcan2  11583  reim0  11609  imval2  11642  cjreim2  11653  cjdivap  11658  cnrecnv  11659  rennim  11751  resqrexlemnm  11767  remsqsqrt  11781  sqrtdiv  11791  sqrtmsq  11794  sqabsadd  11804  sqabssub  11805  absreim  11817  absdivap  11819  absnid  11822  sqabs  11831  abslt  11837  absle  11838  recvalap  11846  abssub  11850  maxabslemlub  11956  infxrnegsupex  12012  mulcn2  12061  reccn2ap  12062  cjcn2  12065  summodclem3  12130  summodclem2a  12131  summodc  12133  zsumdc  12134  fsum3  12137  fisumss  12142  fsumcl2lem  12148  fsumm1  12166  fsum1p  12168  isummulc2  12176  telfsumo  12216  binomlem  12233  bcxmas  12239  arisum  12248  trireciplem  12250  trirecip  12251  geolim2  12262  georeclim  12263  cvgratnnlemfm  12279  cvgratz  12282  mertenslemi1  12285  clim2divap  12290  prodmodclem3  12325  prodmodclem2a  12326  zproddc  12329  fprodseq  12333  fprodssdc  12340  fprod1p  12349  efcan  12426  efexp  12432  efzval  12433  efgt0  12434  eftlub  12440  efltim  12448  resinval  12465  recosval  12466  cosmul  12495  cos2t  12500  cos2tsin  12501  cos01bnd  12508  cos12dec  12518  eirraplem  12527  muldvds1  12566  dvdsexp  12611  oexpneg  12627  divalglemqt  12669  divalglemeunn  12671  divalglemeuneg  12673  divalgmod  12677  flodddiv4t2lthalf  12689  bitsmod  12706  bitsinv1lem  12711  gcdid0  12740  gcdaddm  12744  dvdsgcdidd  12754  rpmulgcd  12786  sqgcd  12789  algcvg  12809  eucalgcvga  12819  eucalg  12820  dvdslcm  12830  lcmeq0  12832  lcmgcd  12839  qredeu  12858  sqnprm  12897  divgcdodd  12904  sqrt2irrlem  12922  sqpweven  12936  2sqpwodd  12937  divnumden  12957  hashdvds  12982  phimullem  12986  eulerthlemrprm  12990  eulerthlemth  12993  odzdvds  13007  pythagtriplem3  13029  pythagtriplem4  13030  pythagtriplem14  13039  pythagtriplem19  13044  pcpremul  13055  pceulem  13056  pcqdiv  13069  pcaddlem  13101  fldivp1  13110  1arithlem4  13128  4sqlem10  13149  mul4sqlem  13155  4sqlem11  13163  4sqlem15  13167  4sqlem16  13168  4sqlem17  13169  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemic  13233  ballotfilem1c  13234  ballotfilemfrceq  13255  ballotfilemrinv0  13259  ennnfonelemhf1o  13287  strslssd  13382  ressbas2d  13405  ressinbasd  13411  topnidg  13589  lidrideqd  13684  grpidd  13686  grprida  13690  gzsumress  13695  ismndd  13733  grpidd2  13829  grpinvid1  13840  grpinvid2  13841  grppnpcan2  13882  grpnpncan  13883  dfgrp3mlem  13886  grpsubpropd2  13893  mhmid  13901  mhmmnd  13902  mulgsubcl  13922  mulgneg  13926  mulgaddcomlem  13931  mulginvinv  13934  mulgdirlem  13939  mulgdir  13940  mulgass  13945  mulgmodid  13947  grpissubg  13980  eqgcpbl  14014  ghmid  14035  ghmmulg  14042  resghm  14046  invghm  14116  gsum0cmn  14137  mgptopng  14211  srgisid  14273  ringidss  14317  ringcom  14319  opprsubgg  14373  unitgrp  14406  1rinv  14418  0unit  14419  rhmdvdsr  14465  lringuplu  14486  subrngpropd  14507  subrgpropd  14544  lmod0vs  14641  lmodvsmmulgdi  14643  lmodvneg1  14650  lmodcom  14653  lmodsubvs  14663  lmodsubdir  14665  lmodpropd  14669  lspsnsub  14741  lspsneq0b  14747  lsppropd  14752  rlmscabas  14780  lidlbas  14798  zringmulg  14916  restopnb  15265  txcnmpt  15357  cnmpt1t  15369  blhalf  15492  xmspropd  15561  mspropd  15562  mpomulcn  15650  ivthreinc  15729  limcimolemlt  15748  dvfre  15794  dveflem  15810  dvef  15811  ply1termlem  15826  plymullem1  15832  sin2kpi  15895  cos2kpi  15896  sin2pim  15897  cos2pim  15898  ptolemy  15908  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  sinq12gt0  15914  tangtx  15922  sincosq1eq  15923  abssinper  15930  sinkpi  15931  relogeftb  15949  relogoprlem  15952  relogexp  15956  log2tlbndlog2  16065  birthdaylem2  16071  birthdaylem3  16072  pellexlem1  16074  mpodvdsmulf1o  16087  mersenne  16094  perfectlem1  16096  perfectlem2  16097  perfect  16098  lgsval2lem  16112  lgsdir2lem4  16133  lgsdirprm  16136  lgsdilem2  16138  gausslemma2dlem7  16170  lgseisenlem4  16175  lgsquadlem1  16179  lgsquadlem2  16180  lgsquad2lem1  16183  lgsquad2lem2  16184  2sqlem4  16220  2sqlem6  16222  2sqlem8  16225  clwwlknonel  16656  eupth2fi  16703  dichmul0orlem2  16737  dichmul0orlem3  16738  dichmul0orlem4  16739  peano3nninf  17024  nninfsel  17034  nninffeq  17037  isomninnlem  17053  cvgcmp2nlemabs  17055  trilpolemlt1  17064  trirec0xor  17068  qdiff  17072  ismkvnnlem  17076