Theorem eqtr2 1499

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 1498	. 2 |- A = C
4	3	eqcomi 1482	1 |- C = A

Syntax hints:   = wceq 958

This theorem is referenced by:  3eqtrr 1503  3eqtr4r 1509  dfun3 2249  symdif1 2268  dfsn2 2424  prprc1 2456  unidif0 2744  abssexg 2753  epfrc 2939  xpindi 3276  xpindir 3277  dmcnvcnv 3342  rncnvcnv 3343  dfrn4 3498  co01 3515  tz7.44-2 3935  oarec 4202  sbthlem8 4460  mapenlem2 4496  unifiOLD 4570  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  trcl 4655  rankxplim2 4723  eqneg 5806  zeot 6201  seq1seq0t 6545  sqrlem11 6684  crne0 6740  crrecz 6742  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 7468  ruclem10 7520  ruclem11 7521  ismeti 7799  0met 7822  cnmetba 7900  remetba 7906  iscau 7933  xplmi 7970  xplmi2 7971  xplm 7972  xpcn 7973  oprcn 7974  bopcnlem3 7980  bopcn 7982  fsumcnlem 7986  abscn 8339  ajfval 8465  ip1ilem 8481  ipasslem10 8495  sincos4thpi 8705  cosh111lem1 8709  pilog 8763  normlem6 8976  dfhnorm2 8983  norm3dif 9009  hhsssh2 9135  occllem1 9168  projlem4 9184  projlem18 9198  pjthlem1 9214  h1de2 9471  spansnj 9586  pjnel 9663  lnopunilem1 9930  lnophmlem2 9937  pjclem1 10118  mdslmd3 10254  atabs 10323  ghomsn 10383  cayleylem3 10406  cmphmp 10507  1cat 10663

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