Theorem bctr 173

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 125	. . 3 b = ((b ∩ c) ∪ (b ∩ c⊥ ))
3		bctr.1	. . 3 a = b
4	3	ran 71	. . . 4 (a ∩ c) = (b ∩ c)
5	3	ran 71	. . . 4 (a ∩ c⊥ ) = (b ∩ c⊥ )
6	4, 5	2or 67	. . 3 ((a ∩ c) ∪ (a ∩ c⊥ )) = ((b ∩ c) ∪ (b ∩ c⊥ ))
7	2, 3, 6	3tr1 60	. 2 a = ((a ∩ c) ∪ (a ∩ c⊥ ))
8	7	df-c1 124	1 a C c

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

This theorem is referenced by:  coman2 178  wwfh1 208  wwfh2 209  wwfh4 211  comor2 444  gsth2 472  gstho 473  gt1 474  i3bi 478  oi3ai3 485  ud4lem3 567  comi12 689  u4lem4 741  3vcom 795  1oa 802  orbi 824  mlaconj4 826  comanblem1 852  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