Theorem cbtr 182

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

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) ∪ (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) ∪ (a ∩ b⊥ )) = ((a ∩ c) ∪ (a ∩ c⊥ ))
8	2, 7	ax-r2 36	. 2 a = ((a ∩ c) ∪ (a ∩ c⊥ ))
9	8	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:  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