Theorem eqtr2d 1500

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
eqtr2d	|- (ph -> C = A)

Proof of Theorem eqtr2d

Step	Hyp	Ref	Expression
1		eqtr2d.1	. . 3 |- (ph -> A = B)
2		eqtr2d.2	. . 3 |- (ph -> B = C)
3	1, 2	eqtrd 1499	. 2 |- (ph -> A = C)
4	3	eqcomd 1472	1 |- (ph -> C = A)

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  3eqtrrd 1504  3eqtr2rd 1506  onsucmin 3062  sbthlem3 4429  rankxpsuc 4687  aceq6b 4714  cnegextlem3 5319  cnegext 5320  submul2t 5432  divadddivt 5740  zaddclt 6112  ceim1lt 6192  shftf 6288  icoshftf1oi 6342  seq1seqz 6473  imret 6710  cjdiv 6826  bcpasc 6907  fsumsplit 6958  fsum2mul 6975  binomlem1 7004  climshft 7041  climmullem5 7060  climsub 7066  clim2serzt 7070  clim2serz 7081  geoisumr 7178  cvgratlem1ALT 7182  cvgratlem1 7185  efcj 7278  efivalt 7389  infxpidmlem4 7498  ntrval2 7628  blin 7792  ioo2bl 7851  grpidinvlem2 7983  subgres 8054  vcz 8126  vcoprne 8136  nvmtri 8238  cnnvm 8251  nvnd 8257  ipid 8297  ipnm 8298  ipipcj 8302  ipasslem2 8422  ipasslem4 8424  ipsubdir 8439  ubthlem12 8471  minveclem19 8494  minveclem21 8496  htthlem9 8558  effoi 8666  effoiOLD 8667  explogt 8694  reexplogt 8695  explogtOLD 8713  hvaddsubvalt 8823  pjspansnt 9417  osumlem2 9496  pjot 9533  unoplint 9760  adjadjt 9776  hmoplint 9782  eigvect 9802  lnopeq 9848  nmcopexlem5 9870  lnfnsub 9890  nmcfnexlem5 9899  riesz3 9910  cnlnadjlem7 9921  branmfnt 9951  kbass2t 9962  kbass6t 9966  leoprf2t 9972  leoprft 9973  pjnmop 9986  hmopidmchlem 9989  hmopidmch 9990  mdslmd1lem1 10160  mdslmd1lem2 10161  superpos 10189  2wsms 10474

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain