Theorem bctr 181

Description: Transitive inference.

Hypotheses

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

Assertion

Ref	Expression
bctr	a C c

Proof of Theorem bctr

Step	Hyp	Ref	Expression
1		bctr.2	. . . 4 b C c
2	1	df-c2 133	. . 3 b = ((b ^ c) v (b ^ c'))
3		bctr.1	. . 3 a = b
4	3	ran 78	. . . 4 (a ^ c) = (b ^ c)
5	3	ran 78	. . . 4 (a ^ c') = (b ^ c')
6	4, 5	2or 72	. . 3 ((a ^ c) v (a ^ c')) = ((b ^ c) v (b ^ c'))
7	2, 3, 6	3tr1 63	. 2 a = ((a ^ c) v (a ^ c'))
8	7	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:  coman2 186  wwfh1 216  wwfh2 217  wwfh4 219  comor2 462  gsth2 490  gstho 491  gt1 492  i3bi 496  oi3ai3 503  ud4lem3 585  comi12 707  u4lem4 759  3vcom 813  1oa 820  orbi 842  mlaconj4 844  comanblem1 870  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