Theorem 3tr1 60

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 34	. . 3 b = d
5	2, 4	ax-r2 35	. 2 a = d
6	1, 5	ax-r2 35	1 c = d

Syntax hints:   = wb 1

This theorem is referenced by:  3tr2 61  con1 63  lor 66  ancom 68  anass 69  lan 70  ran 71  or32 75  an32 76  or4 77  an4 78  oran 79  dfnb 87  bicom 88  lbi 89  rbi 90  an0 100  biid 108  conb 114  di 118  omlem1 119  omlem2 120  bctr 173  cmtrcom 182  wwcomd 206  wwfh1 208  wwfh2 209  ka4lemo 220  ska3 224  skr0 234  lei3 238  mccune2 239  i3id 243  li3 244  ri3 245  ud1lem0a 247  ud1lem0b 248  ud2lem0a 250  ud2lem0b 251  ud4lem0a 254  ud4lem0b 255  ud5lem0a 256  ud5lem0b 257  i1i2 258  i2i1 259  i3i4 262  i5con 264  i1id 267  wql2lem5 284  womle2a 287  nomb41 291  nomb32 292  nomcon0 293  nomcon1 294  nomcon2 295  nomcon3 296  nomcon4 297  nom10 299  nom11 300  nom12 301  nom13 302  nom14 303  nom15 304  nom20 305  nom21 306  nom22 307  nom23 308  nom24 309  nom25 310  nom30 311  nom40 317  nom41 318  nom42 319  nom43 320  nom44 321  nom45 322  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  nom55 328  nom60 329  lei2 338  omla 429  oml5 431  oml5a 432  comcom 435  comcom5 440  fh1 451  fh2 452  fh1r 455  fh2r 456  fh3r 457  fh4r 458  fh2c 459  fh4c 460  fh1rc 461  fh2rc 462  fh3rc 463  fh4rc 464  comcmtr1 476  i0cmtrcom 477  i3bi 478  dfi3b 481  oi3ai3 485  i3lem3 488  i3abs1 504  i3abs3 506  i3th1 525  i3con 533  ud3lem1 552  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud4lem3a 565  ud5lem1b 569  u4lemle2 700  u1lembi 702  u2lembi 703  u5lembi 707  u12lembi 708  u21lembi 709  u1lemn1b 712  u1lem3var1 713  u4lem1n 724  u4lem6 750  u5lem6 751  u12lem 753  u1lem11 762  u3lem11 768  bi1o1a 780  biao 781  i2i1i1 782  3vth4 789  3vth5 790  3vth7 792  3vth9 794  3vded22 800  3vded3 801  1oa 802  2oalem1 807  2oath1 808  2oath1i1 809  mlaoml 815  salem1 819  orbi 824  mlaconj4 826  mlaconj 827  negantlem2 831  negantlem6 836  negantlem8 838  negant0 839  negant2 840  neg3antlem2 847  neg3ant1 848  elimconslem 849  elimcons 850  comanblem2 853  mhlem 858  mh 861  mhcor1 870  cancellem 873  go2n6 881  gomaex3lem2 895  gomaex3lem3 896  gomaex3lem4 897  oa23 916  oa3-2lemb 959  oa3-4lem 963  oa3-5lem 964  oa3-u1lem 965  oa3-1to5 973  oath1 984  4oath1 1020

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

metamath.org