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  4327  eusvnf  4548  f00  5525  f1imacnv  5597  foimacnv  5598  f1ococnv1  5609  funfvdm  5705  fvmptdf  5730  fndmdif  5748  funopsn  5825  acexmidlemph  6006  acexmidlemab  6007  ovmpodf  6148  fvmpopr2d  6153  oprssov  6159  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  oav2  6626  omv2  6628  fnsnsplitdc  6668  ecopovtrn  6796  ecopovtrng  6799  map0b  6851  en1  6968  ssenen  7032  fidifsnen  7052  dif1en  7063  undifdc  7111  fidcenumlemr  7148  ordiso2  7228  nninfninc  7316  nnnninfeq2  7322  nninfisollemne  7324  finomni  7333  exmidomni  7335  fodjum  7339  exmidaclem  7416  distrnqg  7600  1qec  7601  prarloclemarch2  7632  nnnq0lem1  7659  nqpnq0nq  7666  distrnq0  7672  prarloclemlt  7706  prmuloclemcalc  7778  ltaprg  7832  prplnqu  7833  recexprlem1ssl  7846  recexprlem1ssu  7847  ltmprr  7855  cauappcvgprlemopl  7859  caucvgprlemopl  7882  caucvgprprlemopl  7910  caucvgprprlemexb  7920  prsrlem1  7955  ltsosr  7977  mulgt0sr  7991  recidpipr  8069  recriota  8103  nntopi  8107  axcaucvglemres  8112  addlid  8311  readdcan  8312  muladd11r  8328  add32r  8332  cnegexlem2  8348  cnegex  8350  pncan2  8379  addsubass  8382  subadd23  8384  addsub12  8385  subid  8391  subid1  8392  npncan  8393  nppcan3  8396  subsub  8402  nppcan2  8403  nnncan2  8409  npncan3  8410  pnpcan  8411  negdi  8429  mvlraddd  8536  mvlladdd  8537  pnpncand  8547  subdi  8557  mulsub  8573  mulsub2  8574  eqord1  8656  recexap  8826  div32ap  8865  divsubdirap  8881  divmuldivap  8885  divdivdivap  8886  divmuleqap  8890  divcanap6  8892  dmdcanap  8895  divsubdivap  8901  div2negap  8908  div2subap  9010  mvllmulapd  9015  prodgt0gt0  9024  cju  9134  zneo  9574  infrenegsupex  9821  qreccl  9869  mul2lt0rlt0  9987  xnpcan  10100  fzosn  10443  modqid  10604  modqm1p1mod0  10630  modqltm1p1mod  10631  modqmul1  10632  modaddmodup  10642  modaddmodlo  10643  modqsubdir  10648  iseqf1olemkle  10752  iseqf1olemklt  10753  seq3f1olemstep  10769  seq3f1oleml  10771  seqf1oglem2  10775  seqfeq3  10784  seq3distr  10787  expineg2  10803  expm1t  10822  expadd  10836  expaddzaplem  10837  expmulzap  10840  sqsubswap  10854  subsq2  10902  binom2sub  10908  binom3  10912  facndiv  10994  bcval5  11018  bcn2p1  11025  bcnm1  11027  pfxccatpfx2  11311  2shfti  11385  shftcan2  11389  reim0  11415  imval2  11448  cjreim2  11458  cjdivap  11463  cnrecnv  11464  rennim  11556  resqrexlemnm  11572  remsqsqrt  11586  sqrtdiv  11596  sqrtmsq  11599  sqabsadd  11609  sqabssub  11610  absreim  11622  absdivap  11624  absnid  11627  sqabs  11636  abslt  11642  absle  11643  recvalap  11651  abssub  11655  maxabslemlub  11761  infxrnegsupex  11817  mulcn2  11866  reccn2ap  11867  cjcn2  11870  summodclem3  11934  summodclem2a  11935  summodc  11937  zsumdc  11938  fsum3  11941  fisumss  11946  fsumcl2lem  11952  fsumm1  11970  fsum1p  11972  isummulc2  11980  telfsumo  12020  binomlem  12037  bcxmas  12043  arisum  12052  trireciplem  12054  trirecip  12055  geolim2  12066  georeclim  12067  cvgratnnlemfm  12083  cvgratz  12086  mertenslemi1  12089  clim2divap  12094  prodmodclem3  12129  prodmodclem2a  12130  zproddc  12133  fprodseq  12137  fprodssdc  12144  fprod1p  12153  efcan  12230  efexp  12236  efzval  12237  efgt0  12238  eftlub  12244  efltim  12252  resinval  12269  recosval  12270  cosmul  12299  cos2t  12304  cos2tsin  12305  cos01bnd  12312  cos12dec  12322  eirraplem  12331  muldvds1  12370  dvdsexp  12415  oexpneg  12431  divalglemqt  12473  divalglemeunn  12475  divalglemeuneg  12477  divalgmod  12481  flodddiv4t2lthalf  12493  bitsmod  12510  bitsinv1lem  12515  gcdid0  12544  gcdaddm  12548  dvdsgcdidd  12558  rpmulgcd  12590  sqgcd  12593  algcvg  12613  eucalgcvga  12623  eucalg  12624  dvdslcm  12634  lcmeq0  12636  lcmgcd  12643  qredeu  12662  sqnprm  12701  divgcdodd  12708  sqrt2irrlem  12726  sqpweven  12740  2sqpwodd  12741  divnumden  12761  hashdvds  12786  phimullem  12790  eulerthlemrprm  12794  eulerthlemth  12797  odzdvds  12811  pythagtriplem3  12833  pythagtriplem4  12834  pythagtriplem14  12843  pythagtriplem19  12848  pcpremul  12859  pceulem  12860  pcqdiv  12873  pcaddlem  12905  fldivp1  12914  1arithlem4  12932  4sqlem10  12953  mul4sqlem  12959  4sqlem11  12967  4sqlem15  12971  4sqlem16  12972  4sqlem17  12973  ennnfonelemhf1o  13027  strslssd  13122  ressbas2d  13144  ressinbasd  13150  topnidg  13328  lidrideqd  13457  grpidd  13459  grprida  13463  gsumress  13471  ismndd  13513  grpidd2  13617  grpinvid1  13628  grpinvid2  13629  grppnpcan2  13670  grpnpncan  13671  dfgrp3mlem  13674  grpsubpropd2  13681  mhmid  13695  mhmmnd  13696  mulgsubcl  13716  mulgneg  13720  mulgaddcomlem  13725  mulginvinv  13728  mulgdirlem  13733  mulgdir  13734  mulgass  13739  mulgmodid  13741  grpissubg  13774  eqgcpbl  13808  ghmid  13829  ghmmulg  13836  resghm  13840  invghm  13909  gsumfzmptfidmadd  13919  mgptopng  13935  srgisid  13992  ringidss  14035  ringcom  14037  opprsubgg  14090  unitgrp  14123  1rinv  14135  0unit  14136  rhmdvdsr  14182  lringuplu  14203  subrngpropd  14223  subrgpropd  14260  lmod0vs  14328  lmodvsmmulgdi  14330  lmodvneg1  14337  lmodcom  14340  lmodsubvs  14350  lmodsubdir  14352  lmodpropd  14356  lspsnsub  14428  lspsneq0b  14434  lsppropd  14439  rlmscabas  14467  lidlbas  14485  zringmulg  14605  restopnb  14898  txcnmpt  14990  cnmpt1t  15002  blhalf  15125  xmspropd  15194  mspropd  15195  mpomulcn  15283  ivthreinc  15362  limcimolemlt  15381  dvfre  15427  dveflem  15443  dvef  15444  ply1termlem  15459  plymullem1  15465  sin2kpi  15528  cos2kpi  15529  sin2pim  15530  cos2pim  15531  ptolemy  15541  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  tangtx  15555  sincosq1eq  15556  abssinper  15563  sinkpi  15564  relogeftb  15582  relogoprlem  15585  relogexp  15589  mpodvdsmulf1o  15707  mersenne  15714  perfectlem1  15716  perfectlem2  15717  perfect  15718  lgsval2lem  15732  lgsdir2lem4  15753  lgsdirprm  15756  lgsdilem2  15758  gausslemma2dlem7  15790  lgseisenlem4  15795  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2lem1  15803  lgsquad2lem2  15804  2sqlem4  15840  2sqlem6  15842  2sqlem8  15845  clwwlknonel  16241  peano3nninf  16559  nninfsel  16569  nninffeq  16572  isomninnlem  16584  cvgcmp2nlemabs  16586  trilpolemlt1  16595  trirec0xor  16599  ismkvnnlem  16606  gfsum0  16632