Theorem eqtr2d 1506

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 1505	. 2 |- (ph -> A = C)
4	3	eqcomd 1478	1 |- (ph -> C = A)

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  3eqtrrd 1510  3eqtr2rd 1512  onsucmin 3068  sbthlem3 4438  rankxpsuc 4698  aceq6b 4725  cnegextlem3 5330  cnegext 5331  submul2t 5443  divadddivt 5750  zaddclt 6122  ceim1lt 6204  shftf 6301  icoshftf1oi 6355  seq1seqz 6486  imret 6725  cjdiv 6841  bcpasc 6922  fsumsplit 6973  fsum2mul 6990  binomlem1 7019  climshft 7057  climmullem5 7077  climsub 7083  clim2serzt 7087  clim2serz 7098  geoisumr 7195  cvgratlem1ALT 7199  cvgratlem1 7202  efcj 7295  efivalt 7406  infxpidmlem4 7515  ntrval2 7646  blin 7814  ioo2bl 7874  grpidinvlem2 8011  subgres 8081  vcz 8153  vcoprne 8162  nvmtri 8263  cnnvm 8277  nvnd 8283  ipid 8325  ipnm 8326  ipipcj 8330  ipasslem2 8450  ipasslem4 8452  ipsubdir 8467  ubthlem12 8499  minveclem19 8522  minveclem21 8524  htthlem9 8586  effoi 8700  explogt 8727  reexplogt 8728  hvaddsubvalt 8857  pjspansnt 9457  osumlem2 9536  pjot 9573  unoplint 9801  adjadjt 9817  hmoplint 9823  eigvect 9843  lnopeq 9889  nmcopexlem5 9911  lnfnsub 9931  nmcfnexlem5 9940  riesz3 9951  cnlnadjlem7 9962  branmfnt 9994  kbass2t 10006  kbass6t 10010  leoprf2t 10016  leoprft 10017  pjnmop 10031  hmopidmchlem 10034  hmopidmch 10035  mdslmd1lem1 10208  mdslmd1lem2 10209  superpos 10237  2wsms 10546

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 1458

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

Copyright terms: Public domain