Theorem 3tr2 61

Description: Transitive inference useful for eliminating definitions.

Hypotheses

Ref	Expression
3tr2.1	a = b
3tr2.2	a = c
3tr2.3	b = d

Assertion

Ref	Expression
3tr2	c = d

Proof of Theorem 3tr2

Step	Hyp	Ref	Expression
1		3tr2.1	. 2 a = b
2		3tr2.2	. . 3 a = c
3	2	ax-r1 34	. 2 c = a
4		3tr2.3	. . 3 b = d
5	4	ax-r1 34	. 2 d = b
6	1, 3, 5	3tr1 60	1 c = d

Syntax hints:   = wb 1

This theorem is referenced by:  or12 73  an12 74  omlem1 119  letr 129  lecon 146  wwoml2 204  wwoml3 205  sklem 222  ska8 228  wql2lem 280  wql2lem5 284  wql1 285  oaidlem1 286  womle2a 287  nom21 306  2vwomlem 347  wr5-2v 348  wdf-c2 366  woml6 418  r3a 422  oml5 431  oml5a 432  oml2 433  oml3 434  comcom 435  com3i 449  fh3 453  fh4 454  oml4 469  oml6 470  gsth 471  cmtr1com 475  i3bi 478  i3lem3 488  i3lem4 489  lem4 493  i3le 497  i3abs1 504  i3abs3 506  i3th1 525  i3orlem6 539  ud4lem1a 559  ud4lem1c 561  u3lemnana 629  u5lemnana 631  u1lemnab 632  u2lemnab 633  u3lemnab 634  u4lemnab 635  u5lemnab 636  u1lemnanb 637  u2lemnanb 638  u3lemnanb 639  u4lemnanb 640  u5lemnanb 641  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u1lemnona 647  u2lemnona 648  u3lemnona 649  u4lemnona 650  u5lemnona 651  u1lemnob 652  u2lemnob 653  u3lemnob 654  u4lemnob 655  u5lemnob 656  u1lemnonb 657  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  i1com 690  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  u21lembi 709  u4lem6 750  u5lem6 751  u1lem11 762  u3lem11 768  u3lemax4 778  3vth4 789  3vth7 792  3vded21 799  3vded3 801  1oa 802  1oaii 806  2oalem1 807  1oath1i1u 810  3vroa 813  mlaoml 815  sac 817  sa5 818  bi3 821  bi4 822  orbi 824  mlaconj4 826  negantlem2 831  negantlem5 835  negantlem7 837  negant0 839  negant2 840  negantlem9 841  negant5 845  neg3antlem1 846  neg3antlem2 847  elimconslem 849  elimcons 850  comanblem1 852  comanblem2 853  mhlem1 859  mhcor1 870  oago3.29 871  govar 876  go2n6 881  gomaex3lem1 894  gomaex3lem8 901  oaidlem2 911  oaidlem2g 912  distoa 924  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oalii 982  oalem1 985  oagen1b 995  4oagen1b 1022

This theorem was proved from axioms:  ax-r1 34  ax-r2 35

metamath.org