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

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
StepHypRef Expression
1 bctr.2 . . . 4 b C c
21df-c2 133 . . 3 b = ((bc) ∪ (bc ))
3 bctr.1 . . 3 a = b
43ran 78 . . . 4 (ac) = (bc)
53ran 78 . . . 4 (ac ) = (bc )
64, 52or 72 . . 3 ((ac) ∪ (ac )) = ((bc) ∪ (bc ))
72, 3, 63tr1 63 . 2 a = ((ac) ∪ (ac ))
87df-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:  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
  Copyright terms: Public domain W3C validator