Theorem eqtr2d 1511

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

Syntax hints:   -> wi 3   = wceq 958

This theorem is referenced by:  3eqtrrd 1515  3eqtr2rd 1517  onsucmin 3078  sbthlem3 4455  rankxpsuc 4725  aceq6b 4752  cnegextlem3 5359  cnegext 5360  submul2t 5472  divadddivt 5786  zaddclt 6167  ceim1lt 6251  fldivt 6256  shftf 6352  icoshftf1oi 6410  seq1seqz 6542  imret 6774  cjdiv 6888  bcpasc 6969  fsumsplit 7020  fsum2mul 7037  binomlem1 7066  climshft 7104  climmullem5 7124  climsub 7130  clim2serzt 7134  clim2serz 7145  geoisumr 7243  cvgratlem1ALT 7247  cvgratlem1 7250  efcj 7336  efivalt 7447  infxpidmlem4 7556  ntrval2 7683  blin 7849  ioo2bl 7909  grpidinvlem2 8046  subgres 8113  vcz 8185  vcoprne 8194  nvmtri 8295  cnnvm 8309  nvnd 8315  ipid 8359  ipnm 8360  ipipcj 8364  ipasslem2 8487  ipasslem4 8489  ipsubdir 8504  ubthlem12 8536  minveclem19 8559  minveclem21 8561  htthlem9 8624  sinkpi 8692  abssinper 8707  sineq0 8708  effoi 8740  explogt 8767  reexplogt 8768  hvaddsubvalt 8897  pjspansnt 9495  osumlem2 9574  pjot 9611  unoplint 9839  adjadjt 9855  hmoplint 9861  eigvect 9881  lnopeq 9928  nmcopexlem5 9950  lnfnsub 9970  nmcfnexlem5 9979  riesz3 9990  cnlnadjlem7 10001  branmfnt 10033  kbass2t 10045  kbass6t 10049  leoprf2t 10055  leoprft 10056  pjnmop 10070  hmopidmchlem 10073  hmopidmch 10074  mdslmd1lem1 10247  mdslmd1lem2 10248  superpos 10276  2wsms 10601

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain