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  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  oav2  6741  omv2  6743  fnsnsplitdc  6783  ecopovtrn  6911  ecopovtrng  6914  map0b  6973  en1  7092  ssenen  7158  fidifsnen  7178  dif1en  7189  undifdc  7237  fidcenumlemr  7279  isfsuppf  7298  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  9758  infrenegsupex  10010  qreccl  10058  mul2lt0rlt0  10177  xnpcan  10291  fzosn  10640  modqid  10807  modqm1p1mod0  10833  modqltm1p1mod  10834  modqmul1  10835  modaddmodup  10845  modaddmodlo  10846  modqsubdir  10851  iseqf1olemkle  10955  iseqf1olemklt  10956  seq3f1olemstep  10972  seq3f1oleml  10974  seqf1oglem2  10978  seqfeq3  10987  seq3distr  10990  expineg2  11006  expm1t  11025  expadd  11039  expaddzaplem  11040  expmulzap  11043  sqsubswap  11057  subsq2  11105  binom2sub  11111  binom3  11115  resq01  11116  facndiv  11199  bcval5  11223  bcn2p1  11231  bcnm1  11233  hashpwfi  11291  hashfibclem  11304  pfxccatpfx2  11531  2shfti  11618  shftcan2  11622  reim0  11648  imval2  11681  cjreim2  11692  cjdivap  11697  cnrecnv  11698  rennim  11790  resqrexlemnm  11806  remsqsqrt  11820  sqrtdiv  11830  sqrtmsq  11833  sqabsadd  11843  sqabssub  11844  absreim  11856  absdivap  11858  absnid  11861  sqabs  11871  abslt  11877  absle  11878  recvalap  11886  abssub  11890  maxabslemlub  11996  infxrnegsupex  12054  mulcn2  12103  reccn2ap  12104  cjcn2  12107  summodclem3  12172  summodclem2a  12173  summodc  12175  zsumdc  12176  fsum3  12179  fisumss  12184  fsumcl2lem  12190  fsumm1  12208  fsum1p  12210  isummulc2  12218  telfsumo  12258  binomlem  12275  bcxmas  12281  arisum  12290  trireciplem  12292  trirecip  12293  geolim2  12304  georeclim  12305  cvgratnnlemfm  12321  cvgratz  12324  mertenslemi1  12327  clim2divap  12332  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodssdc  12382  fprod1p  12391  efcan  12468  efexp  12474  efzval  12475  efgt0  12476  eftlub  12482  efltim  12490  resinval  12507  recosval  12508  cosmul  12537  cos2t  12542  cos2tsin  12543  cos01bnd  12550  cos12dec  12560  eirraplem  12569  muldvds1  12608  dvdsexp  12653  oexpneg  12669  divalglemqt  12711  divalglemeunn  12713  divalglemeuneg  12715  divalgmod  12719  flodddiv4t2lthalf  12731  bitsmod  12748  bitsinv1lem  12753  gcdid0  12782  gcdaddm  12786  dvdsgcdidd  12796  rpmulgcd  12828  sqgcd  12831  algcvg  12851  eucalgcvga  12861  eucalg  12862  dvdslcm  12872  lcmeq0  12874  lcmgcd  12881  qredeu  12900  sqnprm  12940  divgcdodd  12947  sqrt2irrlem  12965  sqpweven  12980  2sqpwodd  12981  divnumden  13001  hashdvds  13028  phimullem  13032  eulerthlemrprm  13036  eulerthlemth  13039  odzdvds  13053  pythagtriplem3  13075  pythagtriplem4  13076  pythagtriplem14  13085  pythagtriplem19  13090  pcpremul  13101  pceulem  13102  pcqdiv  13115  pcaddlem  13147  fldivp1  13156  1arithlem4  13174  4sqlem10  13195  mul4sqlem  13201  4sqlem11  13209  4sqlem15  13213  4sqlem16  13214  4sqlem17  13215  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemfrceq  13330  ballotfilemrinv0  13334  ennnfonelemhf1o  13362  strslssd  13457  ressbas2d  13481  ressinbasd  13487  topnidg  13665  lidrideqd  13760  grpidd  13762  grprida  13766  gzsumress  13771  ismndd  13809  grpidd2  13905  grpinvid1  13916  grpinvid2  13917  grppnpcan2  13958  grpnpncan  13959  dfgrp3mlem  13962  grpsubpropd2  13969  mhmid  13977  mhmmnd  13978  mulgsubcl  13998  mulgneg  14002  mulgaddcomlem  14007  mulginvinv  14010  mulgdirlem  14015  mulgdir  14016  mulgass  14021  mulgmodid  14023  grpissubg  14056  eqgcpbl  14090  ghmid  14111  ghmmulg  14118  resghm  14122  cntrsubgnsg  14175  invghm  14223  gsum0cmn  14244  gsumresfi  14263  gsum2dfilem2  14272  mgptopng  14335  srgisid  14397  ringidss  14441  ringcom  14443  opprsubgg  14499  unitgrp  14532  1rinv  14544  0unit  14545  rhmdvdsr  14591  lringuplu  14612  subrngpropd  14633  subrgpropd  14670  lmod0vs  14767  lmodvsmmulgdi  14769  lmodvneg1  14776  lmodcom  14779  lmodsubvs  14789  lmodsubdir  14791  lmodpropd  14795  lspsnsub  14867  lspsneq0b  14873  lsppropd  14878  rlmscabas  14906  lidlbas  14924  zringmulg  15042  psr1fi  15225  mvrclfi  15238  restopnb  15440  txcnmpt  15532  cnmpt1t  15544  blhalf  15667  xmspropd  15736  mspropd  15737  mpomulcn  15825  ivthreinc  15904  limcimolemlt  15923  dvfre  15969  dveflem  15985  dvef  15986  ply1termlem  16001  plymullem1  16007  sin2kpi  16071  cos2kpi  16072  sin2pim  16073  cos2pim  16074  ptolemy  16084  sincosq2sgn  16087  sincosq3sgn  16088  sincosq4sgn  16089  sinq12gt0  16090  tangtx  16098  sincosq1eq  16099  abssinper  16106  sinkpi  16107  sineq0re  16109  root1idef  16117  relogeftb  16127  relogoprlem  16131  relogexp  16135  rpcxpmul2z  16181  log2tlbndlog2  16253  birthdaylem2  16259  birthdaylem3  16260  pellexlem1  16262  efchtqdvds  16298  ppiqp1le  16300  ppiqltx  16314  mpodvdsmulf1o  16317  ppiqub  16326  chtqub  16329  mersenne  16330  perfectlem1  16332  perfectlem2  16333  perfect  16334  bposlem6  16349  bposlem9  16352  lgsval2lem  16367  lgsdir2lem4  16388  lgsdirprm  16391  lgsdilem2  16393  gausslemma2dlem7  16425  lgseisenlem4  16430  lgsquadlem1  16434  lgsquadlem2  16435  lgsquad2lem1  16438  lgsquad2lem2  16439  2sqlem4  16475  2sqlem6  16477  2sqlem8  16480  clwwlknonel  16911  eupth2fi  16958  dichmul0orlem2  16992  dichmul0orlem3  16993  dichmul0orlem4  16994  peano3nninf  17289  nninfsel  17299  nninffeq  17302  isomninnlem  17318  cvgcmp2nlemabs  17320  trilpolemlt1  17330  trirec0xor  17334  qdiff  17338  ismkvnnlem  17342