Theorem eqtr3d 1506

Description: An equality transitivity equality deduction.

Hypotheses

Ref	Expression
eqtr3d.1	|- (ph -> A = B)
eqtr3d.2	|- (ph -> A = C)

Assertion

Ref	Expression
eqtr3d	|- (ph -> B = C)

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 |- (ph -> A = B)
2	1	eqcomd 1477	. 2 |- (ph -> B = A)
3		eqtr3d.2	. 2 |- (ph -> A = C)
4	2, 3	eqtrd 1504	1 |- (ph -> B = C)

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  3eqtrrd 1509  3eqtr3d 1512  3eqtr3rd 1513  csbnestg 2032  uneqin 2252  f00 3648  f1imacnv 3696  f1ococnv1 3700  fvsnun2 3787  oprssoprval 4025  caoprmo 4062  oaabs 4242  map0b 4333  mapsn 4335  en1 4413  ssenen 4490  1qec 5048  halfpq 5062  pn0sr 5190  mulgt0sr 5194  cnegextlem2 5326  cnegext 5328  csbnegg 5344  subadd23t 5365  addsub12t 5366  subnegt 5374  pncan2t 5378  npcant 5379  npncant 5380  subdit 5407  subsub2t 5441  subsubt 5442  nnncan1t 5447  nnncan2t 5448  nppcan2t 5450  mulsubt 5457  recext 5665  divcan4t 5727  divsubdirt 5739  divmuldivt 5744  divdivdivt 5749  divcan6t 5755  qrecclt 6219  2shft 6297  shftcan1t 6299  seqzval2t 6493  expm1t 6523  expaddt 6535  expsubt 6537  expordit 6539  subsqt 6581  subsq2t 6582  imcjt 6762  sqabsaddt 6791  sqabssubt 6792  absreimt 6800  absdivz 6802  absnidt 6806  recvalz 6833  abs1m 6849  ser1absdiflem 6874  facndivt 6888  bcpasc 6915  serzfsum 6950  serz0 6999  binomlem5 7016  bcxmaslem2 7021  bcxmas 7022  iserzshft2 7052  climrecl 7055  climge0 7057  climaddlem3 7060  climcj 7094  geoser 7177  cjcncf 7221  mulc1cncf 7222  efcant 7318  efexpt 7322  efnn0valt 7323  resinvalt 7383  recosvalt 7384  cos2tt 7413  sin01bndlem3 7419  cos01bndlem3 7421  iincld 7629  metcnss 7850  metcnss2 7851  grpidinvlem1 7998  grpidinvlem3 8000  grpinvid1 8022  grpinvid2 8023  isgrp2i 8026  grpnpncan 8044  resgrprn 8045  abldivdiv 8060  subgid 8072  cnaddabl 8078  ghgrpilem3 8087  vc2 8126  vcsubdir 8127  vcm 8142  vcnegneg 8145  nvpncan 8229  nvnpcan 8232  nvnncan 8235  nvdif 8245  nvpi 8246  nvge0 8254  imsmetlem 8274  ip0l 8318  ipasslem2 8435  ipasslem4 8437  ipasslem9 8442  ubthlem8 8480  minveclem19 8507  minveclem35 8523  minveclem36 8524  htthlem9 8571  sinperlem1 8624  sin2pim 8630  cos2pim 8631  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  sincosq1eq 8645  shftefif1olem 8680  effoi 8684  eflogt 8699  logeft 8701  relogoprlem 8708  relogexpt 8713  hvaddid2t 8831  hvmul0t 8832  hvnegidt 8835  hvm1negt 8840  hvpncan2t 8848  hvpncan3t 8850  hvsubdistr2t 8856  hhph 8984  chdmj1t 9390  h1de2b 9415  h1de2bOLD 9416  spansncol 9430  h1datom 9444  fh1t 9501  fh2t 9502  5oalem1 9539  3oalem2 9548  pjvect 9581  pjocvect 9582  pjds 9597  mayete3 9613  hosubnegt 9673  hosubsub2t 9678  hosubsubt 9683  cnvunopt 9781  unopadjt 9782  kbmult 9818  nlelch 9932  riesz3 9933  riesz4 9934  nmopcoadj 9972  branmfnt 9976  cnvbramult 9986  leopnmidt 10009  nmopleidt 10010  hmopidmpj 10018  pjclem4 10065  pj3s 10073  hstoct 10087  hst1ht 10092  hstlet 10095  sto1 10101  superpos 10218  cvexchlem 10232  atoml 10246  atord 10248  irredlem3 10256  mdsymlem1 10267  dmdbr5at 10284  cdj3lem3 10299  2wsms 10510

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain