Theorem 3tr2 64

Description: Transitive inference useful for eliminating definitions. (Contributed by NM, 10-Aug-1997.)

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 was proved from axioms:  ax-r1 35  ax-r2 36

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  1094  mldual  1124  ml2i  1125  mldual2i  1127  vneulem12  1142  vneulemexp  1148  modexp  1152  dp15lemf  1159  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208