Theorem 3tr1 63

Description: Transitive inference useful for introducing definitions.

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 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  4oath1 1040  lem3.3.4 1052  lem3.3.6 1055  lem3.3.7i0e1 1056  lem3.3.7i0e2 1057  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem3.3.7i5e2 1072  lem4.6.6i0j1 1085  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  lem4.6.6i1j0 1089  lem4.6.6i1j3 1091  lem4.6.6i2j0 1092  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j0 1097  lem4.6.6i4j2 1098  lem4.6.7 1100  wdwom 1103

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

Copyright terms: Public domain