Theorem eqtr2d 1926

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

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  3eqtrrd 1930  3eqtrrdOLD 1931  3eqtr2rd 1933  onsucmin 3901  ac6sfilem3 5508  sbthlem3 5512  rankxpsuc 5826  aceq6b 5904  cnegexlem3 6501  cnegex 6502  submul2 6625  divadddiv 6960  zaddcl 7374  ceim1l 7490  fldiv 7497  flmod 7506  intfrac 7507  flmulnn0 7508  flmulnn0OLD 7509  modcyc2 7517  moddi 7520  icoshftf1oii 7578  shftf 7764  seq1seqz 7784  imre 8023  mulre 8027  cjdivi 8140  bcpasci 8221  fsumsplit 8280  fsum2mul 8297  binomlem1 8326  climshfti 8364  climmullem5 8384  climsub 8390  clim2serz 8394  clim2serzi 8405  geoisumr 8505  cvgratlem1ALT 8509  cvgratlem1 8512  efcji 8598  efival 8712  infxpidmlem4 8824  ntrval2 8962  blin 9129  ioo2bl 9190  grpidinvlem2 9329  gxid 9396  subgres 9426  isga 9450  isga2 9452  vcz 9521  vcoprne 9530  nvmtri 9631  cnnvm 9645  nvnd 9651  ipid 9702  ipnm 9703  ipipcj 9707  ipasslem2 9832  ipasslem4 9834  ipsubdir 9849  ubthlem12 9883  ubthlem12OLD 9884  minveclem19 9908  minveclem21 9910  htthlem9 9975  abssinper 10062  coskpi 10064  sineq0 10065  sineq0OLD 10066  sineq0re 10067  effoi 10099  explog 10126  reexplog 10127  upxp 10225  uptx 10226  2txcn 10229  hvaddsubval 10534  pjspansn 11133  osumlem2 11214  pjo 11251  unoplin 11481  adjadj 11497  hmoplin 11503  eigvec1 11523  lnopeqi 11570  nmcopexlem5 11592  lnfnsubi 11612  nmcfnexlem5 11621  riesz3i 11632  cnlnadjlem7 11643  branmfn 11675  branmfnOLD 11676  kbass2 11688  kbass6 11692  leoprf2 11698  leoprf 11699  pjnmopi 11719  hmopidmchlem 11722  hmopidmchi 11723  mdslmd1lem1 11897  mdslmd1lem2 11898  superpos 11926  bnj1387 13526  svs3 14830  2wsms 15008  lvsovso 15038  idsubfun 15206  alexsublem1 15437  flimfcnp 15602  upixp 15729  cnss 15892  blbnd 15943  ismtycnv 15949  ismtyhmeo 15951  ismtybndlem 15952  rrnmet 16016  pcoass 16085  omllaw3 16966  cmtcomlem 16969  cmtbr3 16975  omlfh3 16979  grpidinvlem2NEW 17110  pol1 17323  paddatcl 17358  poml4 17361

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain