Theorem eqtr3d 2269

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

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

This theorem is referenced by:  3eqtr3d  2275  3eqtr3rd  2276  3eqtr3a  2291  opth  4358  eusvnf  4579  f00  5564  f1imacnv  5636  foimacnv  5637  f1ococnv1  5648  funfvdm  5745  fvmptdf  5770  fndmdif  5788  funopsn  5865  acexmidlemph  6051  acexmidlemab  6052  ovmpodf  6193  fvmpopr2d  6198  oprssov  6204  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  oav2  6709  omv2  6711  fnsnsplitdc  6751  ecopovtrn  6879  ecopovtrng  6882  map0b  6934  en1  7052  ssenen  7118  fidifsnen  7138  dif1en  7149  undifdc  7197  fidcenumlemr  7238  ordiso2  7339  nninfninc  7427  nnnninfeq2  7433  nninfisollemne  7435  finomni  7444  exmidomni  7446  fodjum  7450  exmidaclem  7528  distrnqg  7718  1qec  7719  prarloclemarch2  7750  nnnq0lem1  7777  nqpnq0nq  7784  distrnq0  7790  prarloclemlt  7824  prmuloclemcalc  7896  ltaprg  7950  prplnqu  7951  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  cauappcvgprlemopl  7977  caucvgprlemopl  8000  caucvgprprlemopl  8028  caucvgprprlemexb  8038  prsrlem1  8073  ltsosr  8095  mulgt0sr  8109  recidpipr  8187  recriota  8221  nntopi  8225  axcaucvglemres  8230  addlid  8429  readdcan  8430  muladd11r  8446  add32r  8450  cnegexlem2  8466  cnegex  8468  pncan2  8497  addsubass  8500  subadd23  8502  addsub12  8503  subid  8509  subid1  8510  npncan  8511  nppcan3  8514  subsub  8520  nppcan2  8521  nnncan2  8527  npncan3  8528  pnpcan  8529  negdi  8547  mvlraddd  8654  mvlladdd  8655  pnpncand  8665  subdi  8676  mulsub  8692  mulsub2  8693  eqord1  8775  recexap  8945  div32ap  8986  divsubdirap  9002  divmuldivap  9006  divdivdivap  9007  divmuleqap  9011  divcanap6  9013  dmdcanap  9016  divsubdivap  9022  div2negap  9029  div2subap  9131  mvllmulapd  9136  prodgt0gt0  9145  cju  9255  zneo  9700  infrenegsupex  9947  qreccl  9995  mul2lt0rlt0  10113  xnpcan  10227  fzosn  10575  modqid  10738  modqm1p1mod0  10764  modqltm1p1mod  10765  modqmul1  10766  modaddmodup  10776  modaddmodlo  10777  modqsubdir  10782  iseqf1olemkle  10886  iseqf1olemklt  10887  seq3f1olemstep  10903  seq3f1oleml  10905  seqf1oglem2  10909  seqfeq3  10918  seq3distr  10921  expineg2  10937  expm1t  10956  expadd  10970  expaddzaplem  10971  expmulzap  10974  sqsubswap  10988  subsq2  11036  binom2sub  11042  binom3  11046  resq01  11047  facndiv  11129  bcval5  11153  bcn2p1  11161  bcnm1  11163  hashpwfi  11221  hashfibclem  11234  pfxccatpfx2  11457  2shfti  11544  shftcan2  11548  reim0  11574  imval2  11607  cjreim2  11618  cjdivap  11623  cnrecnv  11624  rennim  11716  resqrexlemnm  11732  remsqsqrt  11746  sqrtdiv  11756  sqrtmsq  11759  sqabsadd  11769  sqabssub  11770  absreim  11782  absdivap  11784  absnid  11787  sqabs  11796  abslt  11802  absle  11803  recvalap  11811  abssub  11815  maxabslemlub  11921  infxrnegsupex  11977  mulcn2  12026  reccn2ap  12027  cjcn2  12030  summodclem3  12095  summodclem2a  12096  summodc  12098  zsumdc  12099  fsum3  12102  fisumss  12107  fsumcl2lem  12113  fsumm1  12131  fsum1p  12133  isummulc2  12141  telfsumo  12181  binomlem  12198  bcxmas  12204  arisum  12213  trireciplem  12215  trirecip  12216  geolim2  12227  georeclim  12228  cvgratnnlemfm  12244  cvgratz  12247  mertenslemi1  12250  clim2divap  12255  prodmodclem3  12290  prodmodclem2a  12291  zproddc  12294  fprodseq  12298  fprodssdc  12305  fprod1p  12314  efcan  12391  efexp  12397  efzval  12398  efgt0  12399  eftlub  12405  efltim  12413  resinval  12430  recosval  12431  cosmul  12460  cos2t  12465  cos2tsin  12466  cos01bnd  12473  cos12dec  12483  eirraplem  12492  muldvds1  12531  dvdsexp  12576  oexpneg  12592  divalglemqt  12634  divalglemeunn  12636  divalglemeuneg  12638  divalgmod  12642  flodddiv4t2lthalf  12654  bitsmod  12671  bitsinv1lem  12676  gcdid0  12705  gcdaddm  12709  dvdsgcdidd  12719  rpmulgcd  12751  sqgcd  12754  algcvg  12774  eucalgcvga  12784  eucalg  12785  dvdslcm  12795  lcmeq0  12797  lcmgcd  12804  qredeu  12823  sqnprm  12862  divgcdodd  12869  sqrt2irrlem  12887  sqpweven  12901  2sqpwodd  12902  divnumden  12922  hashdvds  12947  phimullem  12951  eulerthlemrprm  12955  eulerthlemth  12958  odzdvds  12972  pythagtriplem3  12994  pythagtriplem4  12995  pythagtriplem14  13004  pythagtriplem19  13009  pcpremul  13020  pceulem  13021  pcqdiv  13034  pcaddlem  13066  fldivp1  13075  1arithlem4  13093  4sqlem10  13114  mul4sqlem  13120  4sqlem11  13128  4sqlem15  13132  4sqlem16  13133  4sqlem17  13134  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemic  13198  ballotfilem1c  13199  ballotfilemfrceq  13220  ballotfilemrinv0  13224  ennnfonelemhf1o  13252  strslssd  13347  ressbas2d  13369  ressinbasd  13375  topnidg  13553  lidrideqd  13648  grpidd  13650  grprida  13654  gsumress  13662  ismndd  13702  grpidd2  13800  grpinvid1  13811  grpinvid2  13812  grppnpcan2  13853  grpnpncan  13854  dfgrp3mlem  13857  grpsubpropd2  13864  mhmid  13872  mhmmnd  13873  mulgsubcl  13893  mulgneg  13897  mulgaddcomlem  13902  mulginvinv  13905  mulgdirlem  13910  mulgdir  13911  mulgass  13916  mulgmodid  13918  grpissubg  13951  eqgcpbl  13985  ghmid  14006  ghmmulg  14013  resghm  14017  invghm  14086  gsumfzmptfidmadd  14096  gfsum0  14108  mgptopng  14172  srgisid  14233  ringidss  14276  ringcom  14278  opprsubgg  14332  unitgrp  14365  1rinv  14377  0unit  14378  rhmdvdsr  14424  lringuplu  14445  subrngpropd  14466  subrgpropd  14503  lmod0vs  14599  lmodvsmmulgdi  14601  lmodvneg1  14608  lmodcom  14611  lmodsubvs  14621  lmodsubdir  14623  lmodpropd  14627  lspsnsub  14699  lspsneq0b  14705  lsppropd  14710  rlmscabas  14738  lidlbas  14756  zringmulg  14876  restopnb  15176  txcnmpt  15268  cnmpt1t  15280  blhalf  15403  xmspropd  15472  mspropd  15473  mpomulcn  15561  ivthreinc  15640  limcimolemlt  15659  dvfre  15705  dveflem  15721  dvef  15722  ply1termlem  15737  plymullem1  15743  sin2kpi  15806  cos2kpi  15807  sin2pim  15808  cos2pim  15809  ptolemy  15819  sincosq2sgn  15822  sincosq3sgn  15823  sincosq4sgn  15824  sinq12gt0  15825  tangtx  15833  sincosq1eq  15834  abssinper  15841  sinkpi  15842  relogeftb  15860  relogoprlem  15863  relogexp  15867  pellexlem1  15975  mpodvdsmulf1o  15988  mersenne  15995  perfectlem1  15997  perfectlem2  15998  perfect  15999  lgsval2lem  16013  lgsdir2lem4  16034  lgsdirprm  16037  lgsdilem2  16039  gausslemma2dlem7  16071  lgseisenlem4  16076  lgsquadlem1  16080  lgsquadlem2  16081  lgsquad2lem1  16084  lgsquad2lem2  16085  2sqlem4  16121  2sqlem6  16123  2sqlem8  16126  clwwlknonel  16557  eupth2fi  16604  dichmul0orlem2  16638  dichmul0orlem3  16639  dichmul0orlem4  16640  peano3nninf  16925  nninfsel  16935  nninffeq  16938  isomninnlem  16954  cvgcmp2nlemabs  16956  trilpolemlt1  16965  trirec0xor  16969  qdiff  16973  ismkvnnlem  16977