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  4323  eusvnf  4544  f00  5519  f1imacnv  5591  foimacnv  5592  f1ococnv1  5603  funfvdm  5699  fvmptdf  5724  fndmdif  5742  funopsn  5819  acexmidlemph  6000  acexmidlemab  6001  ovmpodf  6142  fvmpopr2d  6147  oprssov  6153  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  oav2  6617  omv2  6619  fnsnsplitdc  6659  ecopovtrn  6787  ecopovtrng  6790  map0b  6842  en1  6959  ssenen  7020  fidifsnen  7040  dif1en  7049  undifdc  7094  fidcenumlemr  7130  ordiso2  7210  nninfninc  7298  nnnninfeq2  7304  nninfisollemne  7306  finomni  7315  exmidomni  7317  fodjum  7321  exmidaclem  7398  distrnqg  7582  1qec  7583  prarloclemarch2  7614  nnnq0lem1  7641  nqpnq0nq  7648  distrnq0  7654  prarloclemlt  7688  prmuloclemcalc  7760  ltaprg  7814  prplnqu  7815  recexprlem1ssl  7828  recexprlem1ssu  7829  ltmprr  7837  cauappcvgprlemopl  7841  caucvgprlemopl  7864  caucvgprprlemopl  7892  caucvgprprlemexb  7902  prsrlem1  7937  ltsosr  7959  mulgt0sr  7973  recidpipr  8051  recriota  8085  nntopi  8089  axcaucvglemres  8094  addlid  8293  readdcan  8294  muladd11r  8310  add32r  8314  cnegexlem2  8330  cnegex  8332  pncan2  8361  addsubass  8364  subadd23  8366  addsub12  8367  subid  8373  subid1  8374  npncan  8375  nppcan3  8378  subsub  8384  nppcan2  8385  nnncan2  8391  npncan3  8392  pnpcan  8393  negdi  8411  mvlraddd  8518  mvlladdd  8519  pnpncand  8529  subdi  8539  mulsub  8555  mulsub2  8556  eqord1  8638  recexap  8808  div32ap  8847  divsubdirap  8863  divmuldivap  8867  divdivdivap  8868  divmuleqap  8872  divcanap6  8874  dmdcanap  8877  divsubdivap  8883  div2negap  8890  div2subap  8992  mvllmulapd  8997  prodgt0gt0  9006  cju  9116  zneo  9556  infrenegsupex  9797  qreccl  9845  mul2lt0rlt0  9963  xnpcan  10076  fzosn  10419  modqid  10579  modqm1p1mod0  10605  modqltm1p1mod  10606  modqmul1  10607  modaddmodup  10617  modaddmodlo  10618  modqsubdir  10623  iseqf1olemkle  10727  iseqf1olemklt  10728  seq3f1olemstep  10744  seq3f1oleml  10746  seqf1oglem2  10750  seqfeq3  10759  seq3distr  10762  expineg2  10778  expm1t  10797  expadd  10811  expaddzaplem  10812  expmulzap  10815  sqsubswap  10829  subsq2  10877  binom2sub  10883  binom3  10887  facndiv  10969  bcval5  10993  bcn2p1  11000  bcnm1  11002  pfxccatpfx2  11277  2shfti  11350  shftcan2  11354  reim0  11380  imval2  11413  cjreim2  11423  cjdivap  11428  cnrecnv  11429  rennim  11521  resqrexlemnm  11537  remsqsqrt  11551  sqrtdiv  11561  sqrtmsq  11564  sqabsadd  11574  sqabssub  11575  absreim  11587  absdivap  11589  absnid  11592  sqabs  11601  abslt  11607  absle  11608  recvalap  11616  abssub  11620  maxabslemlub  11726  infxrnegsupex  11782  mulcn2  11831  reccn2ap  11832  cjcn2  11835  summodclem3  11899  summodclem2a  11900  summodc  11902  zsumdc  11903  fsum3  11906  fisumss  11911  fsumcl2lem  11917  fsumm1  11935  fsum1p  11937  isummulc2  11945  telfsumo  11985  binomlem  12002  bcxmas  12008  arisum  12017  trireciplem  12019  trirecip  12020  geolim2  12031  georeclim  12032  cvgratnnlemfm  12048  cvgratz  12051  mertenslemi1  12054  clim2divap  12059  prodmodclem3  12094  prodmodclem2a  12095  zproddc  12098  fprodseq  12102  fprodssdc  12109  fprod1p  12118  efcan  12195  efexp  12201  efzval  12202  efgt0  12203  eftlub  12209  efltim  12217  resinval  12234  recosval  12235  cosmul  12264  cos2t  12269  cos2tsin  12270  cos01bnd  12277  cos12dec  12287  eirraplem  12296  muldvds1  12335  dvdsexp  12380  oexpneg  12396  divalglemqt  12438  divalglemeunn  12440  divalglemeuneg  12442  divalgmod  12446  flodddiv4t2lthalf  12458  bitsmod  12475  bitsinv1lem  12480  gcdid0  12509  gcdaddm  12513  dvdsgcdidd  12523  rpmulgcd  12555  sqgcd  12558  algcvg  12578  eucalgcvga  12588  eucalg  12589  dvdslcm  12599  lcmeq0  12601  lcmgcd  12608  qredeu  12627  sqnprm  12666  divgcdodd  12673  sqrt2irrlem  12691  sqpweven  12705  2sqpwodd  12706  divnumden  12726  hashdvds  12751  phimullem  12755  eulerthlemrprm  12759  eulerthlemth  12762  odzdvds  12776  pythagtriplem3  12798  pythagtriplem4  12799  pythagtriplem14  12808  pythagtriplem19  12813  pcpremul  12824  pceulem  12825  pcqdiv  12838  pcaddlem  12870  fldivp1  12879  1arithlem4  12897  4sqlem10  12918  mul4sqlem  12924  4sqlem11  12932  4sqlem15  12936  4sqlem16  12937  4sqlem17  12938  ennnfonelemhf1o  12992  strslssd  13087  ressbas2d  13109  ressinbasd  13115  topnidg  13293  lidrideqd  13422  grpidd  13424  grprida  13428  gsumress  13436  ismndd  13478  grpidd2  13582  grpinvid1  13593  grpinvid2  13594  grppnpcan2  13635  grpnpncan  13636  dfgrp3mlem  13639  grpsubpropd2  13646  mhmid  13660  mhmmnd  13661  mulgsubcl  13681  mulgneg  13685  mulgaddcomlem  13690  mulginvinv  13693  mulgdirlem  13698  mulgdir  13699  mulgass  13704  mulgmodid  13706  grpissubg  13739  eqgcpbl  13773  ghmid  13794  ghmmulg  13801  resghm  13805  invghm  13874  gsumfzmptfidmadd  13884  mgptopng  13900  srgisid  13957  ringidss  14000  ringcom  14002  opprsubgg  14055  unitgrp  14088  1rinv  14100  0unit  14101  rhmdvdsr  14147  lringuplu  14168  subrngpropd  14188  subrgpropd  14225  lmod0vs  14293  lmodvsmmulgdi  14295  lmodvneg1  14302  lmodcom  14305  lmodsubvs  14315  lmodsubdir  14317  lmodpropd  14321  lspsnsub  14393  lspsneq0b  14399  lsppropd  14404  rlmscabas  14432  lidlbas  14450  zringmulg  14570  restopnb  14863  txcnmpt  14955  cnmpt1t  14967  blhalf  15090  xmspropd  15159  mspropd  15160  mpomulcn  15248  ivthreinc  15327  limcimolemlt  15346  dvfre  15392  dveflem  15408  dvef  15409  ply1termlem  15424  plymullem1  15430  sin2kpi  15493  cos2kpi  15494  sin2pim  15495  cos2pim  15496  ptolemy  15506  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  tangtx  15520  sincosq1eq  15521  abssinper  15528  sinkpi  15529  relogeftb  15547  relogoprlem  15550  relogexp  15554  mpodvdsmulf1o  15672  mersenne  15679  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsval2lem  15697  lgsdir2lem4  15718  lgsdirprm  15721  lgsdilem2  15723  gausslemma2dlem7  15755  lgseisenlem4  15760  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem1  15768  lgsquad2lem2  15769  2sqlem4  15805  2sqlem6  15807  2sqlem8  15810  peano3nninf  16403  nninfsel  16413  nninffeq  16416  isomninnlem  16428  cvgcmp2nlemabs  16430  trilpolemlt1  16439  trirec0xor  16443  ismkvnnlem  16450