Theorem 3tr1 63

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

Hypotheses

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

Assertion

Ref	Expression
3tr1	c = d

Proof of Theorem 3tr1

Step	Hyp	Ref	Expression
1		3tr1.2	. 2 c = a
2		3tr1.1	. . 3 a = b
3		3tr1.3	. . . 4 d = b
4	3	ax-r1 35	. . 3 b = d
5	2, 4	ax-r2 36	. 2 a = d
6	1, 5	ax-r2 36	1 c = d

Syntax hints:   = wb 1

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

This theorem is referenced by:  3tr2  64  con1  66  lor  70  ancom  74  anass  76  lan  77  ran  78  or32  82  an32  83  or4  84  an4  86  oran  87  dfnb  95  bicom  96  lbi  97  rbi  98  an0  108  biid  116  conb  122  di  126  omlem1  127  omlem2  128  bctr  181  cmtrcom  190  wwcomd  214  wwfh1  216  wwfh2  217  anorabs  225  ka4lemo  228  ska3  232  skr0  242  lei3  246  mccune2  247  i3id  251  li3  252  ri3  253  ud1lem0a  255  ud1lem0b  256  ud2lem0a  258  ud2lem0b  259  ud4lem0a  262  ud4lem0b  263  ud5lem0a  264  ud5lem0b  265  i1i2  266  i2i1  267  i3i4  270  i5con  272  i1id  275  wql2lem5  292  womle2a  295  nomb41  299  nomb32  300  nomcon0  301  nomcon1  302  nomcon2  303  nomcon3  304  nomcon4  305  nom10  307  nom11  308  nom12  309  nom13  310  nom14  311  nom15  312  nom20  313  nom21  314  nom22  315  nom23  316  nom24  317  nom25  318  nom30  319  nom40  325  nom41  326  nom42  327  nom43  328  nom44  329  nom45  330  nom50  331  nom51  332  nom52  333  nom53  334  nom54  335  nom55  336  nom60  337  lei2  346  k1-6  353  k1-7  354  k1-4  359  omla  447  oml5  449  oml5a  450  comcom  453  comcom5  458  fh1  469  fh2  470  fh1r  473  fh2r  474  fh3r  475  fh4r  476  fh2c  477  fh4c  478  fh1rc  479  fh2rc  480  fh3rc  481  fh4rc  482  comcmtr1  494  i0cmtrcom  495  i3bi  496  dfi3b  499  oi3ai3  503  i3lem3  506  i3abs1  522  i3abs3  524  i3th1  543  i3con  551  ud3lem1  570  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud4lem3a  583  ud5lem1b  587  u4lemle2  718  u1lembi  720  u2lembi  721  u5lembi  725  u12lembi  726  u21lembi  727  u1lemn1b  730  u1lem3var1  731  u4lem1n  742  u4lem6  768  u5lem6  769  u12lem  771  u1lem11  780  u3lem11  786  bi1o1a  798  biao  799  i2i1i1  800  3vth4  807  3vth5  808  3vth7  810  3vth9  812  3vded22  818  3vded3  819  1oa  820  2oalem1  825  2oath1  826  2oath1i1  827  mlaoml  833  salem1  837  orbi  842  mlaconj4  844  mlaconj  845  negantlem2  849  negantlem6  854  negantlem8  856  negant0  857  negant2  858  neg3antlem2  865  neg3ant1  866  elimconslem  867  elimcons  868  comanblem2  871  mhlem  876  mh  879  mhcor1  888  cancellem  891  e2ast2  894  go2n6  901  gomaex3lem2  915  gomaex3lem3  916  gomaex3lem4  917  oa23  936  oa3-2lemb  979  oa3-4lem  983  oa3-5lem  984  oa3-u1lem  985  oa3-1to5  993  oath1  1004  oa3moa3  1029  4oath1  1041  lem3.3.4  1053  lem3.3.6  1056  lem3.3.7i0e1  1057  lem3.3.7i0e2  1058  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem3.3.7i5e2  1073  thm3.8i1lem  1080  lem4.6.6i0j1  1088  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i1j0  1092  lem4.6.6i1j3  1094  lem4.6.6i2j0  1095  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101  lem4.6.7  1103  wdwom  1106  l42modlem1  1149  dp35leme  1173  dp41lemj  1191  xdp41  1198  xxdp41  1201  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208