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  4377  eusvnf  4599  f00  5584  f1imacnv  5656  foimacnv  5657  f1ococnv1  5668  funfvdm  5766  fvmptdf  5793  fndmdif  5814  funopsn  5891  acexmidlemph  6078  acexmidlemab  6079  ovmpodf  6220  fvmpopr2d  6225  oprssov  6231  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  oav2  6736  omv2  6738  fnsnsplitdc  6778  ecopovtrn  6906  ecopovtrng  6909  map0b  6968  en1  7086  ssenen  7152  fidifsnen  7172  dif1en  7183  undifdc  7231  fidcenumlemr  7272  ordiso2  7375  nninfninc  7463  nnnninfeq2  7469  nninfisollemne  7471  finomni  7480  exmidomni  7482  fodjum  7486  exmidaclem  7564  distrnqg  7754  1qec  7755  prarloclemarch2  7786  nnnq0lem1  7813  nqpnq0nq  7820  distrnq0  7826  prarloclemlt  7860  prmuloclemcalc  7932  ltaprg  7986  prplnqu  7987  recexprlem1ssl  8000  recexprlem1ssu  8001  ltmprr  8009  cauappcvgprlemopl  8013  caucvgprlemopl  8036  caucvgprprlemopl  8064  caucvgprprlemexb  8074  prsrlem1  8109  ltsosr  8131  mulgt0sr  8145  recidpipr  8223  recriota  8257  nntopi  8261  axcaucvglemres  8266  addlid  8465  readdcan  8466  muladd11r  8482  add32r  8486  cnegexlem2  8502  cnegex  8504  pncan2  8533  addsubass  8536  subadd23  8538  addsub12  8539  subid  8545  subid1  8546  npncan  8547  nppcan3  8550  subsub  8556  nppcan2  8557  nnncan2  8563  npncan3  8564  pnpcan  8565  negdi  8583  mvlraddd  8690  mvlladdd  8691  pnpncand  8701  subdi  8712  mulsub  8728  mulsub2  8729  eqord1  8811  recexap  8982  div32ap  9023  divsubdirap  9039  divmuldivap  9043  divdivdivap  9044  divmuleqap  9048  divcanap6  9050  dmdcanap  9053  divsubdivap  9059  div2negap  9066  div2subap  9168  mvllmulapd  9173  prodgt0gt0  9182  cju  9292  zneo  9749  infrenegsupex  9996  qreccl  10044  mul2lt0rlt0  10162  xnpcan  10276  fzosn  10625  modqid  10788  modqm1p1mod0  10814  modqltm1p1mod  10815  modqmul1  10816  modaddmodup  10826  modaddmodlo  10827  modqsubdir  10832  iseqf1olemkle  10936  iseqf1olemklt  10937  seq3f1olemstep  10953  seq3f1oleml  10955  seqf1oglem2  10959  seqfeq3  10968  seq3distr  10971  expineg2  10987  expm1t  11006  expadd  11020  expaddzaplem  11021  expmulzap  11024  sqsubswap  11038  subsq2  11086  binom2sub  11092  binom3  11096  resq01  11097  facndiv  11179  bcval5  11203  bcn2p1  11211  bcnm1  11213  hashpwfi  11271  hashfibclem  11284  pfxccatpfx2  11511  2shfti  11598  shftcan2  11602  reim0  11628  imval2  11661  cjreim2  11672  cjdivap  11677  cnrecnv  11678  rennim  11770  resqrexlemnm  11786  remsqsqrt  11800  sqrtdiv  11810  sqrtmsq  11813  sqabsadd  11823  sqabssub  11824  absreim  11836  absdivap  11838  absnid  11841  sqabs  11850  abslt  11856  absle  11857  recvalap  11865  abssub  11869  maxabslemlub  11975  infxrnegsupex  12031  mulcn2  12080  reccn2ap  12081  cjcn2  12084  summodclem3  12149  summodclem2a  12150  summodc  12152  zsumdc  12153  fsum3  12156  fisumss  12161  fsumcl2lem  12167  fsumm1  12185  fsum1p  12187  isummulc2  12195  telfsumo  12235  binomlem  12252  bcxmas  12258  arisum  12267  trireciplem  12269  trirecip  12270  geolim2  12281  georeclim  12282  cvgratnnlemfm  12298  cvgratz  12301  mertenslemi1  12304  clim2divap  12309  prodmodclem3  12344  prodmodclem2a  12345  zproddc  12348  fprodseq  12352  fprodssdc  12359  fprod1p  12368  efcan  12445  efexp  12451  efzval  12452  efgt0  12453  eftlub  12459  efltim  12467  resinval  12484  recosval  12485  cosmul  12514  cos2t  12519  cos2tsin  12520  cos01bnd  12527  cos12dec  12537  eirraplem  12546  muldvds1  12585  dvdsexp  12630  oexpneg  12646  divalglemqt  12688  divalglemeunn  12690  divalglemeuneg  12692  divalgmod  12696  flodddiv4t2lthalf  12708  bitsmod  12725  bitsinv1lem  12730  gcdid0  12759  gcdaddm  12763  dvdsgcdidd  12773  rpmulgcd  12805  sqgcd  12808  algcvg  12828  eucalgcvga  12838  eucalg  12839  dvdslcm  12849  lcmeq0  12851  lcmgcd  12858  qredeu  12877  sqnprm  12916  divgcdodd  12923  sqrt2irrlem  12941  sqpweven  12955  2sqpwodd  12956  divnumden  12976  hashdvds  13001  phimullem  13005  eulerthlemrprm  13009  eulerthlemth  13012  odzdvds  13026  pythagtriplem3  13048  pythagtriplem4  13049  pythagtriplem14  13058  pythagtriplem19  13063  pcpremul  13074  pceulem  13075  pcqdiv  13088  pcaddlem  13120  fldivp1  13129  1arithlem4  13147  4sqlem10  13168  mul4sqlem  13174  4sqlem11  13182  4sqlem15  13186  4sqlem16  13187  4sqlem17  13188  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemic  13252  ballotfilem1c  13253  ballotfilemfrceq  13274  ballotfilemrinv0  13278  ennnfonelemhf1o  13306  strslssd  13401  ressbas2d  13424  ressinbasd  13430  topnidg  13608  lidrideqd  13703  grpidd  13705  grprida  13709  gzsumress  13714  ismndd  13752  grpidd2  13848  grpinvid1  13859  grpinvid2  13860  grppnpcan2  13901  grpnpncan  13902  dfgrp3mlem  13905  grpsubpropd2  13912  mhmid  13920  mhmmnd  13921  mulgsubcl  13941  mulgneg  13945  mulgaddcomlem  13950  mulginvinv  13953  mulgdirlem  13958  mulgdir  13959  mulgass  13964  mulgmodid  13966  grpissubg  13999  eqgcpbl  14033  ghmid  14054  ghmmulg  14061  resghm  14065  invghm  14135  gsum0cmn  14156  mgptopng  14230  srgisid  14292  ringidss  14336  ringcom  14338  opprsubgg  14392  unitgrp  14425  1rinv  14437  0unit  14438  rhmdvdsr  14484  lringuplu  14505  subrngpropd  14526  subrgpropd  14563  lmod0vs  14660  lmodvsmmulgdi  14662  lmodvneg1  14669  lmodcom  14672  lmodsubvs  14682  lmodsubdir  14684  lmodpropd  14688  lspsnsub  14760  lspsneq0b  14766  lsppropd  14771  rlmscabas  14799  lidlbas  14817  zringmulg  14935  restopnb  15284  txcnmpt  15376  cnmpt1t  15388  blhalf  15511  xmspropd  15580  mspropd  15581  mpomulcn  15669  ivthreinc  15748  limcimolemlt  15767  dvfre  15813  dveflem  15829  dvef  15830  ply1termlem  15845  plymullem1  15851  sin2kpi  15915  cos2kpi  15916  sin2pim  15917  cos2pim  15918  ptolemy  15928  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  sinq12gt0  15934  tangtx  15942  sincosq1eq  15943  abssinper  15950  sinkpi  15951  relogeftb  15969  relogoprlem  15973  relogexp  15977  log2tlbndlog2  16088  birthdaylem2  16094  birthdaylem3  16095  pellexlem1  16097  mpodvdsmulf1o  16110  mersenne  16117  perfectlem1  16119  perfectlem2  16120  perfect  16121  lgsval2lem  16141  lgsdir2lem4  16162  lgsdirprm  16165  lgsdilem2  16167  gausslemma2dlem7  16199  lgseisenlem4  16204  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad2lem1  16212  lgsquad2lem2  16213  2sqlem4  16249  2sqlem6  16251  2sqlem8  16254  clwwlknonel  16685  eupth2fi  16732  dichmul0orlem2  16766  dichmul0orlem3  16767  dichmul0orlem4  16768  peano3nninf  17062  nninfsel  17072  nninffeq  17075  isomninnlem  17091  cvgcmp2nlemabs  17093  trilpolemlt1  17102  trirec0xor  17106  qdiff  17110  ismkvnnlem  17114