Theorem eqtr3d 2264

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3d  2270  3eqtr3rd  2271  3eqtr3a  2286  opth  4322  eusvnf  4541  f00  5513  f1imacnv  5585  foimacnv  5586  f1ococnv1  5597  funfvdm  5690  fvmptdf  5715  fndmdif  5733  funopsn  5810  acexmidlemph  5987  acexmidlemab  5988  ovmpodf  6127  fvmpopr2d  6132  oprssov  6138  tfrlemisucaccv  6461  tfr1onlemsucaccv  6477  tfrcllemsucaccv  6490  oav2  6599  omv2  6601  fnsnsplitdc  6641  ecopovtrn  6769  ecopovtrng  6772  map0b  6824  en1  6941  ssenen  7000  fidifsnen  7020  dif1en  7029  undifdc  7074  fidcenumlemr  7110  ordiso2  7190  nninfninc  7278  nnnninfeq2  7284  nninfisollemne  7286  finomni  7295  exmidomni  7297  fodjum  7301  exmidaclem  7378  distrnqg  7562  1qec  7563  prarloclemarch2  7594  nnnq0lem1  7621  nqpnq0nq  7628  distrnq0  7634  prarloclemlt  7668  prmuloclemcalc  7740  ltaprg  7794  prplnqu  7795  recexprlem1ssl  7808  recexprlem1ssu  7809  ltmprr  7817  cauappcvgprlemopl  7821  caucvgprlemopl  7844  caucvgprprlemopl  7872  caucvgprprlemexb  7882  prsrlem1  7917  ltsosr  7939  mulgt0sr  7953  recidpipr  8031  recriota  8065  nntopi  8069  axcaucvglemres  8074  addlid  8273  readdcan  8274  muladd11r  8290  add32r  8294  cnegexlem2  8310  cnegex  8312  pncan2  8341  addsubass  8344  subadd23  8346  addsub12  8347  subid  8353  subid1  8354  npncan  8355  nppcan3  8358  subsub  8364  nppcan2  8365  nnncan2  8371  npncan3  8372  pnpcan  8373  negdi  8391  mvlraddd  8498  mvlladdd  8499  pnpncand  8509  subdi  8519  mulsub  8535  mulsub2  8536  eqord1  8618  recexap  8788  div32ap  8827  divsubdirap  8843  divmuldivap  8847  divdivdivap  8848  divmuleqap  8852  divcanap6  8854  dmdcanap  8857  divsubdivap  8863  div2negap  8870  div2subap  8972  mvllmulapd  8977  prodgt0gt0  8986  cju  9096  zneo  9536  infrenegsupex  9777  qreccl  9825  mul2lt0rlt0  9943  xnpcan  10056  fzosn  10398  modqid  10558  modqm1p1mod0  10584  modqltm1p1mod  10585  modqmul1  10586  modaddmodup  10596  modaddmodlo  10597  modqsubdir  10602  iseqf1olemkle  10706  iseqf1olemklt  10707  seq3f1olemstep  10723  seq3f1oleml  10725  seqf1oglem2  10729  seqfeq3  10738  seq3distr  10741  expineg2  10757  expm1t  10776  expadd  10790  expaddzaplem  10791  expmulzap  10794  sqsubswap  10808  subsq2  10856  binom2sub  10862  binom3  10866  facndiv  10948  bcval5  10972  bcn2p1  10979  bcnm1  10981  pfxccatpfx2  11255  2shfti  11328  shftcan2  11332  reim0  11358  imval2  11391  cjreim2  11401  cjdivap  11406  cnrecnv  11407  rennim  11499  resqrexlemnm  11515  remsqsqrt  11529  sqrtdiv  11539  sqrtmsq  11542  sqabsadd  11552  sqabssub  11553  absreim  11565  absdivap  11567  absnid  11570  sqabs  11579  abslt  11585  absle  11586  recvalap  11594  abssub  11598  maxabslemlub  11704  infxrnegsupex  11760  mulcn2  11809  reccn2ap  11810  cjcn2  11813  summodclem3  11877  summodclem2a  11878  summodc  11880  zsumdc  11881  fsum3  11884  fisumss  11889  fsumcl2lem  11895  fsumm1  11913  fsum1p  11915  isummulc2  11923  telfsumo  11963  binomlem  11980  bcxmas  11986  arisum  11995  trireciplem  11997  trirecip  11998  geolim2  12009  georeclim  12010  cvgratnnlemfm  12026  cvgratz  12029  mertenslemi1  12032  clim2divap  12037  prodmodclem3  12072  prodmodclem2a  12073  zproddc  12076  fprodseq  12080  fprodssdc  12087  fprod1p  12096  efcan  12173  efexp  12179  efzval  12180  efgt0  12181  eftlub  12187  efltim  12195  resinval  12212  recosval  12213  cosmul  12242  cos2t  12247  cos2tsin  12248  cos01bnd  12255  cos12dec  12265  eirraplem  12274  muldvds1  12313  dvdsexp  12358  oexpneg  12374  divalglemqt  12416  divalglemeunn  12418  divalglemeuneg  12420  divalgmod  12424  flodddiv4t2lthalf  12436  bitsmod  12453  bitsinv1lem  12458  gcdid0  12487  gcdaddm  12491  dvdsgcdidd  12501  rpmulgcd  12533  sqgcd  12536  algcvg  12556  eucalgcvga  12566  eucalg  12567  dvdslcm  12577  lcmeq0  12579  lcmgcd  12586  qredeu  12605  sqnprm  12644  divgcdodd  12651  sqrt2irrlem  12669  sqpweven  12683  2sqpwodd  12684  divnumden  12704  hashdvds  12729  phimullem  12733  eulerthlemrprm  12737  eulerthlemth  12740  odzdvds  12754  pythagtriplem3  12776  pythagtriplem4  12777  pythagtriplem14  12786  pythagtriplem19  12791  pcpremul  12802  pceulem  12803  pcqdiv  12816  pcaddlem  12848  fldivp1  12857  1arithlem4  12875  4sqlem10  12896  mul4sqlem  12902  4sqlem11  12910  4sqlem15  12914  4sqlem16  12915  4sqlem17  12916  ennnfonelemhf1o  12970  strslssd  13065  ressbas2d  13087  ressinbasd  13093  topnidg  13271  lidrideqd  13400  grpidd  13402  grprida  13406  gsumress  13414  ismndd  13456  grpidd2  13560  grpinvid1  13571  grpinvid2  13572  grppnpcan2  13613  grpnpncan  13614  dfgrp3mlem  13617  grpsubpropd2  13624  mhmid  13638  mhmmnd  13639  mulgsubcl  13659  mulgneg  13663  mulgaddcomlem  13668  mulginvinv  13671  mulgdirlem  13676  mulgdir  13677  mulgass  13682  mulgmodid  13684  grpissubg  13717  eqgcpbl  13751  ghmid  13772  ghmmulg  13779  resghm  13783  invghm  13852  gsumfzmptfidmadd  13862  mgptopng  13878  srgisid  13935  ringidss  13978  ringcom  13980  opprsubgg  14033  unitgrp  14065  1rinv  14077  0unit  14078  rhmdvdsr  14124  lringuplu  14145  subrngpropd  14165  subrgpropd  14202  lmod0vs  14270  lmodvsmmulgdi  14272  lmodvneg1  14279  lmodcom  14282  lmodsubvs  14292  lmodsubdir  14294  lmodpropd  14298  lspsnsub  14370  lspsneq0b  14376  lsppropd  14381  rlmscabas  14409  lidlbas  14427  zringmulg  14547  restopnb  14840  txcnmpt  14932  cnmpt1t  14944  blhalf  15067  xmspropd  15136  mspropd  15137  mpomulcn  15225  ivthreinc  15304  limcimolemlt  15323  dvfre  15369  dveflem  15385  dvef  15386  ply1termlem  15401  plymullem1  15407  sin2kpi  15470  cos2kpi  15471  sin2pim  15472  cos2pim  15473  ptolemy  15483  sincosq2sgn  15486  sincosq3sgn  15487  sincosq4sgn  15488  sinq12gt0  15489  tangtx  15497  sincosq1eq  15498  abssinper  15505  sinkpi  15506  relogeftb  15524  relogoprlem  15527  relogexp  15531  mpodvdsmulf1o  15649  mersenne  15656  perfectlem1  15658  perfectlem2  15659  perfect  15660  lgsval2lem  15674  lgsdir2lem4  15695  lgsdirprm  15698  lgsdilem2  15700  gausslemma2dlem7  15732  lgseisenlem4  15737  lgsquadlem1  15741  lgsquadlem2  15742  lgsquad2lem1  15745  lgsquad2lem2  15746  2sqlem4  15782  2sqlem6  15784  2sqlem8  15787  peano3nninf  16304  nninfsel  16314  nninffeq  16317  isomninnlem  16329  cvgcmp2nlemabs  16331  trilpolemlt1  16340  trirec0xor  16344  ismkvnnlem  16351