Theorem eqtr2 1496

Description: An equality transitivity inference.

Hypotheses

Ref	Expression
eqtr2.1	|- A = B
eqtr2.2	|- B = C

Assertion

Ref	Expression
eqtr2	|- C = A

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqtr2.1	. . 3 |- A = B
2		eqtr2.2	. . 3 |- B = C
3	1, 2	eqtr 1495	. 2 |- A = C
4	3	eqcomi 1479	1 |- C = A

Syntax hints:   = wceq 956

This theorem is referenced by:  3eqtrr 1500  3eqtr4r 1506  dfun3 2246  symdif1 2265  dfsn2 2420  prprc1 2452  unidif0 2739  abssexg 2747  epfrc 2933  xpindi 3270  xpindir 3271  dmcnvcnv 3336  rncnvcnv 3337  dfrn4 3492  co01 3509  tz7.44-2 3929  oarec 4196  sbthlem8 4454  mapenlem2 4490  unifiOLD 4557  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  trcl 4645  rankxplim2 4713  eqneg 5804  zeot 6199  seq1seq0t 6544  sqrlem11 6683  crne0 6739  crrecz 6741  ipcn 6790  abslem2i 6908  bcpasc2 6967  binomlem6 7071  isumshft2 7205  ege2lem2 7328  ege2le3lem2 7329  efaddlem6 7343  efaddlem16 7353  efge1 7401  efge1p 7402  efcnlem2 7420  sin01bndlem1 7467  ruclem10 7519  ruclem11 7520  ismeti 7802  0met 7825  cnmetba 7903  remetba 7909  iscau 7936  xplmi 7973  xplmi2 7974  xplm 7975  xpcn 7976  oprcn 7977  bopcnlem3 7983  bopcn 7985  fsumcnlem 7989  abscn 8343  ajfval 8469  ip1ilem 8485  ipasslem10 8499  sincos4thpi 8710  cosh111lem1 8714  pilog 8768  normlem6 8981  dfhnorm2 8988  norm3dif 9014  hhsssh2 9140  occllem1 9173  projlem4 9189  projlem18 9203  pjthlem1 9219  h1de2 9476  spansnj 9591  pjnel 9668  lnopunilem1 9935  lnophmlem2 9942  pjclem1 10123  mdslmd3 10259  atabs 10328  ghomsn 10388  cayleylem3 10411  cmphmp 10521  1cat 10692

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