Theorem eqtr3d 1509

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  3eqtrrd 1512  3eqtr3d 1515  3eqtr3rd 1516  csbnestg 2036  uneqin 2256  f00 3657  f1imacnv 3705  f1ococnv1 3709  fvsnun2 3796  oprssoprval 4034  caoprmo 4070  oaabs 4252  map0b 4343  mapsn 4345  en1 4426  ssenen 4504  1qec 5068  halfpq 5082  pn0sr 5210  mulgt0sr 5214  cnegextlem2 5346  cnegext 5348  csbnegg 5364  subadd23t 5385  addsub12t 5386  subnegt 5394  pncan2t 5398  npcant 5399  npncant 5400  subdit 5427  subsub2t 5461  subsubt 5462  nnncan1t 5467  nnncan2t 5468  nppcan2t 5470  mulsubt 5477  recext 5684  divcan4tOLD 5763  divsubdirtOLD 5775  divmuldivt 5780  divdivdivt 5785  divcan6t 5791  qrecclt 6273  2shft 6352  shftcan1t 6354  seqzval2t 6553  expm1t 6583  expaddt 6596  expsubt 6598  expordit 6600  subsqt 6642  subsq2t 6643  imret 6773  imcjt 6819  sqabsaddt 6848  sqabssubt 6849  absreimt 6857  absdivz 6859  absnidt 6863  recvalz 6887  abs1m 6904  ser1absdiflem 6929  facndivt 6943  bcpasc 6969  serzfsum 7004  serz0 7053  binomlem5 7070  bcxmaslem2 7075  bcxmas 7076  iserzshft2 7107  climrecl 7110  climge0 7112  climaddlem3 7116  climcj 7150  geoser 7234  cjcncf 7278  mulc1cncf 7279  efcant 7368  efexpt 7372  efnn0valt 7373  resinvalt 7433  recosvalt 7434  cos2tt 7463  sin01bndlem3 7469  cos01bndlem3 7471  iincld 7679  metcnss 7898  metcnss2 7899  grpidinvlem1 8048  grpidinvlem3 8050  grpinvid1 8072  grpinvid2 8073  isgrp2i 8076  grpnpncan 8094  resgrprn 8095  abldivdiv 8108  subgid 8120  cnaddabl 8126  ghgrpilem3 8135  vc2 8174  vcsubdir 8175  vcm 8190  vcnegneg 8193  nvpncan 8277  nvnpcan 8280  nvnncan 8283  nvdif 8293  nvpi 8294  nvge0 8302  imsmetlem 8323  ip0l 8371  ipasslem2 8491  ipasslem4 8493  ipasslem9 8498  ubthlem8 8536  minveclem19 8563  minveclem35 8579  minveclem36 8580  htthlem9 8628  sinperlem1 8686  sin2pim 8692  cos2pim 8693  sinkpi 8697  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  sinq12gt0t 8708  sincosq1eq 8709  abssinper 8712  sineq0 8713  shftefif1olem 8741  effoi 8745  eflogt 8760  logeft 8762  relogoprlem 8769  relogexpt 8774  hvaddid2t 8892  hvmul0t 8893  hvnegidt 8896  hvm1negt 8901  hvpncan2t 8909  hvpncan3t 8911  hvsubdistr2t 8917  hhph 9045  chdmj1t 9452  h1de2b 9477  spansncol 9491  h1datom 9504  fh1t 9561  fh2t 9562  5oalem1 9599  3oalem2 9608  pjvect 9641  pjocvect 9642  pjds 9657  mayete3 9673  hosubnegt 9733  hosubsub2t 9738  hosubsubt 9743  cnvunopt 9842  unopadjt 9843  kbmult 9879  nlelch 9994  riesz3 9995  riesz4 9996  nmopcoadj 10034  branmfnt 10038  cnvbramult 10048  leopnmidt 10071  nmopleidt 10072  hmopidmpj 10080  pjclem4 10127  pj3s 10135  hstoct 10149  hst1ht 10154  hstlet 10157  sto1 10163  superpos 10281  cvexchlem 10295  atoml 10309  atord 10311  irredlem3 10319  mdsymlem1 10330  dmdbr5at 10349  cdj3lem3 10365  2wsms 10630

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain