Theorem eqtr3d 2228

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr3d  2234  3eqtr3rd  2235  3eqtr3a  2250  opth  4266  eusvnf  4484  f00  5445  f1imacnv  5517  foimacnv  5518  f1ococnv1  5529  funfvdm  5620  fvmptdf  5645  fndmdif  5663  acexmidlemph  5911  acexmidlemab  5912  ovmpodf  6050  oprssov  6060  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  oav2  6516  omv2  6518  fnsnsplitdc  6558  ecopovtrn  6686  ecopovtrng  6689  map0b  6741  en1  6853  ssenen  6907  fidifsnen  6926  dif1en  6935  undifdc  6980  fidcenumlemr  7014  ordiso2  7094  nninfninc  7182  nnnninfeq2  7188  nninfisollemne  7190  finomni  7199  exmidomni  7201  fodjum  7205  exmidaclem  7268  distrnqg  7447  1qec  7448  prarloclemarch2  7479  nnnq0lem1  7506  nqpnq0nq  7513  distrnq0  7519  prarloclemlt  7553  prmuloclemcalc  7625  ltaprg  7679  prplnqu  7680  recexprlem1ssl  7693  recexprlem1ssu  7694  ltmprr  7702  cauappcvgprlemopl  7706  caucvgprlemopl  7729  caucvgprprlemopl  7757  caucvgprprlemexb  7767  prsrlem1  7802  ltsosr  7824  mulgt0sr  7838  recidpipr  7916  recriota  7950  nntopi  7954  axcaucvglemres  7959  addlid  8158  readdcan  8159  muladd11r  8175  add32r  8179  cnegexlem2  8195  cnegex  8197  pncan2  8226  addsubass  8229  subadd23  8231  addsub12  8232  subid  8238  subid1  8239  npncan  8240  nppcan3  8243  subsub  8249  nppcan2  8250  nnncan2  8256  npncan3  8257  pnpcan  8258  negdi  8276  mvlraddd  8383  mvlladdd  8384  pnpncand  8394  subdi  8404  mulsub  8420  mulsub2  8421  eqord1  8502  recexap  8672  div32ap  8711  divsubdirap  8727  divmuldivap  8731  divdivdivap  8732  divmuleqap  8736  divcanap6  8738  dmdcanap  8741  divsubdivap  8747  div2negap  8754  div2subap  8856  mvllmulapd  8861  prodgt0gt0  8870  cju  8980  zneo  9418  infrenegsupex  9659  qreccl  9707  mul2lt0rlt0  9825  xnpcan  9938  fzosn  10272  modqid  10420  modqm1p1mod0  10446  modqltm1p1mod  10447  modqmul1  10448  modaddmodup  10458  modaddmodlo  10459  modqsubdir  10464  iseqf1olemkle  10568  iseqf1olemklt  10569  seq3f1olemstep  10585  seq3f1oleml  10587  seqf1oglem2  10591  seqfeq3  10600  seq3distr  10603  expineg2  10619  expm1t  10638  expadd  10652  expaddzaplem  10653  expmulzap  10656  sqsubswap  10670  subsq2  10718  binom2sub  10724  binom3  10728  facndiv  10810  bcval5  10834  bcn2p1  10841  bcnm1  10843  2shfti  10975  shftcan2  10979  reim0  11005  imval2  11038  cjreim2  11048  cjdivap  11053  cnrecnv  11054  rennim  11146  resqrexlemnm  11162  remsqsqrt  11176  sqrtdiv  11186  sqrtmsq  11189  sqabsadd  11199  sqabssub  11200  absreim  11212  absdivap  11214  absnid  11217  sqabs  11226  abslt  11232  absle  11233  recvalap  11241  abssub  11245  maxabslemlub  11351  infxrnegsupex  11406  mulcn2  11455  reccn2ap  11456  cjcn2  11459  summodclem3  11523  summodclem2a  11524  summodc  11526  zsumdc  11527  fsum3  11530  fisumss  11535  fsumcl2lem  11541  fsumm1  11559  fsum1p  11561  isummulc2  11569  telfsumo  11609  binomlem  11626  bcxmas  11632  arisum  11641  trireciplem  11643  trirecip  11644  geolim2  11655  georeclim  11656  cvgratnnlemfm  11672  cvgratz  11675  mertenslemi1  11678  clim2divap  11683  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodssdc  11733  fprod1p  11742  efcan  11819  efexp  11825  efzval  11826  efgt0  11827  eftlub  11833  efltim  11841  resinval  11858  recosval  11859  cosmul  11888  cos2t  11893  cos2tsin  11894  cos01bnd  11901  cos12dec  11911  eirraplem  11920  muldvds1  11959  dvdsexp  12003  oexpneg  12018  divalglemqt  12060  divalglemeunn  12062  divalglemeuneg  12064  divalgmod  12068  flodddiv4t2lthalf  12078  gcdid0  12117  gcdaddm  12121  dvdsgcdidd  12131  rpmulgcd  12163  sqgcd  12166  algcvg  12186  eucalgcvga  12196  eucalg  12197  dvdslcm  12207  lcmeq0  12209  lcmgcd  12216  qredeu  12235  sqnprm  12274  divgcdodd  12281  sqrt2irrlem  12299  sqpweven  12313  2sqpwodd  12314  divnumden  12334  hashdvds  12359  phimullem  12363  eulerthlemrprm  12367  eulerthlemth  12370  odzdvds  12383  pythagtriplem3  12405  pythagtriplem4  12406  pythagtriplem14  12415  pythagtriplem19  12420  pcpremul  12431  pceulem  12432  pcqdiv  12445  pcaddlem  12477  fldivp1  12486  1arithlem4  12504  4sqlem10  12525  mul4sqlem  12531  4sqlem11  12539  4sqlem15  12543  4sqlem16  12544  4sqlem17  12545  ennnfonelemhf1o  12570  strslssd  12665  ressbas2d  12686  ressinbasd  12692  topnidg  12863  lidrideqd  12964  grpidd  12966  grprida  12970  gsumress  12978  ismndd  13018  grpidd2  13113  grpinvid1  13124  grpinvid2  13125  grppnpcan2  13166  grpnpncan  13167  dfgrp3mlem  13170  grpsubpropd2  13177  mhmid  13185  mhmmnd  13186  mulgsubcl  13206  mulgneg  13210  mulgaddcomlem  13215  mulginvinv  13218  mulgdirlem  13223  mulgdir  13224  mulgass  13229  mulgmodid  13231  grpissubg  13264  eqgcpbl  13298  ghmid  13319  ghmmulg  13326  resghm  13330  invghm  13399  gsumfzmptfidmadd  13409  mgptopng  13425  srgisid  13482  ringidss  13525  ringcom  13527  opprsubgg  13580  unitgrp  13612  1rinv  13624  0unit  13625  rhmdvdsr  13671  lringuplu  13692  subrngpropd  13712  subrgpropd  13749  lmod0vs  13817  lmodvsmmulgdi  13819  lmodvneg1  13826  lmodcom  13829  lmodsubvs  13839  lmodsubdir  13841  lmodpropd  13845  lspsnsub  13917  lspsneq0b  13923  lsppropd  13928  rlmscabas  13956  lidlbas  13974  zringmulg  14086  restopnb  14349  txcnmpt  14441  cnmpt1t  14453  blhalf  14576  xmspropd  14645  mspropd  14646  ivthreinc  14799  limcimolemlt  14818  dvfre  14859  dveflem  14872  dvef  14873  ply1termlem  14888  plymullem1  14894  sin2kpi  14946  cos2kpi  14947  sin2pim  14948  cos2pim  14949  ptolemy  14959  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  tangtx  14973  sincosq1eq  14974  abssinper  14981  sinkpi  14982  relogeftb  15000  relogoprlem  15003  relogexp  15007  lgsval2lem  15126  lgsdir2lem4  15147  lgsdirprm  15150  lgsdilem2  15152  gausslemma2dlem7  15184  lgseisenlem4  15189  lgsquadlem1  15191  2sqlem4  15205  2sqlem6  15207  2sqlem8  15210  peano3nninf  15497  nninfsel  15507  nninffeq  15510  isomninnlem  15520  cvgcmp2nlemabs  15522  trilpolemlt1  15531  trirec0xor  15535  ismkvnnlem  15542