Theorem eqtr3d 1508

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 1479	. 2 |- (ph -> B = A)
3		eqtr3d.2	. 2 |- (ph -> A = C)
4	2, 3	eqtrd 1506	1 |- (ph -> B = C)

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  3eqtrrd 1511  3eqtr3d 1514  3eqtr3rd 1515  csbnestg 2034  uneqin 2254  f00 3654  f1imacnv 3702  f1ococnv1 3706  fvsnun2 3793  oprssoprval 4031  caoprmo 4067  oaabs 4249  map0b 4340  mapsn 4342  en1 4420  ssenen 4497  1qec 5055  halfpq 5069  pn0sr 5197  mulgt0sr 5201  cnegextlem2 5333  cnegext 5335  csbnegg 5351  subadd23t 5372  addsub12t 5373  subnegt 5381  pncan2t 5385  npcant 5386  npncant 5387  subdit 5414  subsub2t 5448  subsubt 5449  nnncan1t 5454  nnncan2t 5455  nppcan2t 5457  mulsubt 5464  recext 5671  divcan4t 5733  divsubdirt 5745  divmuldivt 5750  divdivdivt 5755  divcan6t 5761  qrecclt 6228  2shft 6307  shftcan1t 6309  seqzval2t 6503  expm1t 6533  expaddt 6546  expsubt 6548  expordit 6550  subsqt 6592  subsq2t 6593  imret 6731  imcjt 6780  sqabsaddt 6810  sqabssubt 6811  absreimt 6819  absdivz 6821  absnidt 6825  recvalz 6852  abs1m 6869  ser1absdiflem 6895  facndivt 6909  bcpasc 6937  serzfsum 6972  serz0 7021  binomlem5 7038  bcxmaslem2 7043  bcxmas 7044  iserzshft2 7075  climrecl 7078  climge0 7080  climaddlem3 7085  climcj 7119  geoser 7205  cjcncf 7249  mulc1cncf 7250  efcant 7346  efexpt 7350  efnn0valt 7351  resinvalt 7411  recosvalt 7412  cos2tt 7441  sin01bndlem3 7447  cos01bndlem3 7449  iincld 7658  metcnss 7881  metcnss2 7882  grpidinvlem1 8031  grpidinvlem3 8033  grpinvid1 8055  grpinvid2 8056  isgrp2i 8059  grpnpncan 8077  resgrprn 8078  abldivdiv 8093  subgid 8105  cnaddabl 8111  ghgrpilem3 8120  vc2 8159  vcsubdir 8160  vcm 8175  vcnegneg 8178  nvpncan 8262  nvnpcan 8265  nvnncan 8268  nvdif 8278  nvpi 8279  nvge0 8287  imsmetlem 8309  ip0l 8357  ipasslem2 8475  ipasslem4 8477  ipasslem9 8482  ubthlem8 8520  minveclem19 8547  minveclem35 8563  minveclem36 8564  htthlem9 8611  sinperlem1 8669  sin2pim 8675  cos2pim 8676  sincosq2sgn 8686  sincosq3sgn 8687  sincosq4sgn 8688  sinq12gt0t 8689  sincosq1eq 8690  shftefif1olem 8725  effoi 8729  eflogt 8744  logeft 8746  relogoprlem 8753  relogexpt 8758  hvaddid2t 8876  hvmul0t 8877  hvnegidt 8880  hvm1negt 8885  hvpncan2t 8893  hvpncan3t 8895  hvsubdistr2t 8901  hhph 9032  hhphOLD 9033  chdmj1t 9440  h1de2b 9465  h1de2bOLD 9466  spansncol 9480  h1datom 9494  fh1t 9551  fh2t 9552  5oalem1 9590  3oalem2 9599  pjvect 9632  pjocvect 9633  pjds 9648  mayete3 9664  hosubnegt 9724  hosubsub2t 9729  hosubsubt 9734  cnvunopt 9833  unopadjt 9834  kbmult 9870  nlelch 9985  riesz3 9986  riesz4 9987  nmopcoadj 10025  branmfnt 10029  cnvbramult 10039  leopnmidt 10062  nmopleidt 10063  hmopidmpj 10071  pjclem4 10118  pj3s 10126  hstoct 10140  hst1ht 10145  hstlet 10148  sto1 10154  superpos 10272  cvexchlem 10286  atoml 10300  atord 10302  irredlem3 10310  mdsymlem1 10321  dmdbr5at 10340  cdj3lem3 10356  2wsms 10581

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1459

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

Copyright terms: Public domain