Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  cbtr GIF version

Theorem cbtr 182
 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
StepHypRef Expression
1 cbtr.1 . . . 4 a C b
21df-c2 133 . . 3 a = ((ab) ∪ (ab ))
3 cbtr.2 . . . . 5 b = c
43lan 77 . . . 4 (ab) = (ac)
53ax-r4 37 . . . . 5 b = c
65lan 77 . . . 4 (ab ) = (ac )
74, 62or 72 . . 3 ((ab) ∪ (ab )) = ((ac) ∪ (ac ))
82, 7ax-r2 36 . 2 a = ((ac) ∪ (ac ))
98df-c1 132 1 a C c
 Colors of variables: term 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
 Copyright terms: Public domain W3C validator