Theorem bctr 181

Description: Transitive inference. (Contributed by NM, 30-Aug-1997.)

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) ∪ (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) ∪ (a ∩ c⊥ )) = ((b ∩ c) ∪ (b ∩ c⊥ ))
7	2, 3, 6	3tr1 63	. 2 a = ((a ∩ c) ∪ (a ∩ c⊥ ))
8	7	df-c1 132	1 a C c

Syntax hints:   = wb 1   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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

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