Theorem cbtr 174

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 125	. . 3 a = ((a ^ b) v (a ^ b_|_))
3		cbtr.2	. . . . 5 b = c
4	3	lan 70	. . . 4 (a ^ b) = (a ^ c)
5	3	ax-r4 36	. . . . 5 b_|_ = c_|_
6	5	lan 70	. . . 4 (a ^ b_|_) = (a ^ c_|_)
7	4, 6	2or 67	. . 3 ((a ^ b) v (a ^ b_|_)) = ((a ^ c) v (a ^ c_|_))
8	2, 7	ax-r2 35	. 2 a = ((a ^ c) v (a ^ c_|_))
9	8	df-c1 124	1 a C c

Syntax hints:   = wb 1   C wc 3  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  comid 179  com2an 466  combi 467  nbdi 468  gsth 471  gsth2 472  gstho 473  i3bi 478  comi31 490  com2i3 491  u1lemc1 662  u2lemc1 663  u4lemc1 665  u5lemc1 666  u5lemc1b 667  u1lemc2 668  u2lemc2 669  u4lemc2 671  u5lemc2 672  comi12 689  ublemc2 711  1oa 802  2oath1 808  mlalem 814  orbi 824  comanbn 855  oacom 991  oacom3 993

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

This theorem depends on definitions:  df-a 39  df-c1 124  df-c2 125

metamath.org