Theorem cbtr 182

Description: Transitive inference.

Hypotheses

Ref	Expression
cbtr.1	a C b
cbtr.2	b = c

Assertion

Ref	Expression
cbtr	a C c

Proof of Theorem cbtr

Step	Hyp	Ref	Expression
1		cbtr.1	. . . 4 a C b
2	1	df-c2 133	. . 3 a = ((a ^ b) v (a ^ b'))
3		cbtr.2	. . . . 5 b = c
4	3	lan 77	. . . 4 (a ^ b) = (a ^ c)
5	3	ax-r4 37	. . . . 5 b' = c'
6	5	lan 77	. . . 4 (a ^ b') = (a ^ c')
7	4, 6	2or 72	. . 3 ((a ^ b) v (a ^ b')) = ((a ^ c) v (a ^ c'))
8	2, 7	ax-r2 36	. 2 a = ((a ^ c) v (a ^ c'))
9	8	df-c1 132	1 a C c

Syntax hints:   = wb 1   C wc 3  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  comid 187  com2an 484  combi 485  nbdi 486  gsth 489  gsth2 490  gstho 491  i3bi 496  comi31 508  com2i3 509  u1lemc1 680  u2lemc1 681  u4lemc1 683  u5lemc1 684  u5lemc1b 685  u1lemc2 686  u2lemc2 687  u4lemc2 689  u5lemc2 690  comi12 707  ublemc2 729  1oa 820  2oath1 826  mlalem 832  orbi 842  comanbn 873  oacom 1011  oacom3 1013

This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-c1 132  df-c2 133

Copyright terms: Public domain