Theorem 3tr2 64

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 35	. 2 c = a
4		3tr2.3	. . 3 b = d
5	4	ax-r1 35	. 2 d = b
6	1, 3, 5	3tr1 63	1 c = d

Syntax hints:   = wb 1

This theorem is referenced by:  or12 80  an12 81  omlem1 127  letr 137  lecon 154  wwoml2 212  wwoml3 213  sklem 230  ska8 236  wql2lem 288  wql2lem5 292  wql1 293  oaidlem1 294  womle2a 295  nom21 314  k1-4 359  k1-5 360  2vwomlem 365  wr5-2v 366  wdf-c2 384  woml6 436  r3a 440  oml5 449  oml5a 450  oml2 451  oml3 452  comcom 453  com3i 467  fh3 471  fh4 472  oml4 487  oml6 488  gsth 489  cmtr1com 493  i3bi 496  i3lem3 506  i3lem4 507  lem4 511  i3le 515  i3abs1 522  i3abs3 524  i3th1 543  i3orlem6 557  ud4lem1a 577  ud4lem1c 579  u3lemnana 647  u5lemnana 649  u1lemnab 650  u2lemnab 651  u3lemnab 652  u4lemnab 653  u5lemnab 654  u1lemnanb 655  u2lemnanb 656  u3lemnanb 657  u4lemnanb 658  u5lemnanb 659  u2lemnoa 661  u3lemnoa 662  u4lemnoa 663  u5lemnoa 664  u1lemnona 665  u2lemnona 666  u3lemnona 667  u4lemnona 668  u5lemnona 669  u1lemnob 670  u2lemnob 671  u3lemnob 672  u4lemnob 673  u5lemnob 674  u1lemnonb 675  u3lemnonb 677  u4lemnonb 678  u5lemnonb 679  i1com 708  u1lemle2 715  u2lemle2 716  u4lemle2 718  u5lemle2 719  u21lembi 727  u4lem6 768  u5lem6 769  u1lem11 780  u3lem11 786  u3lemax4 796  3vth4 807  3vth7 810  3vded21 817  3vded3 819  1oa 820  1oaii 824  2oalem1 825  1oath1i1u 828  3vroa 831  mlaoml 833  sac 835  sa5 836  bi3 839  bi4 840  orbi 842  mlaconj4 844  negantlem2 849  negantlem5 853  negantlem7 855  negant0 857  negant2 858  negantlem9 859  negant5 863  neg3antlem1 864  neg3antlem2 865  elimconslem 867  elimcons 868  comanblem1 870  comanblem2 871  mhlem1 877  mhcor1 888  oago3.29 889  e2ast2 894  govar 896  go2n6 901  gomaex3lem1 914  gomaex3lem8 921  oaidlem2 931  oaidlem2g 932  distoa 944  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oalii 1002  oalem1 1005  oagen1b 1015  4oagen1b 1043  lem3.3.4 1053  lem3.3.6 1056  lem3.3.7i0e1 1057  lem3.3.7i1e1 1060  lem3.3.7i2e1 1063  lem4.6.6i1j3 1092  mldual 1122  ml2i 1123  mldual2i 1125  vneulem12 1140  vneulemexp 1146  dplem15f 1153

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

Copyright terms: Public domain