QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ri3 Unicode version
Theorem ri3 253
Description: Introduce Kalmbach implication to the right.
Hypothesis
Ref Expression
ri3.1 a = b
Assertion
Ref Expression
ri3 (a ->3 c) = (b ->3 c)
Proof of Theorem ri3
StepHypRef Expression
1 ri3.1 . . . . . 6 a = b
21ax-r4 37 . . . . 5 a' = b'
32ran 78 . . . 4 (a' ^ c) = (b' ^ c)
42ran 78 . . . 4 (a' ^ c') = (b' ^ c')
53, 42or 72 . . 3 ((a' ^ c) v (a' ^ c')) = ((b' ^ c) v (b' ^ c'))
62ax-r5 38 . . . 4 (a' v c) = (b' v c)
71, 62an 79 . . 3 (a ^ (a' v c)) = (b ^ (b' v c))
85, 72or 72 . 2 (((a' ^ c) v (a' ^ c')) v (a ^ (a' v c))) = (((b' ^ c) v (b' ^ c')) v (b ^ (b' v c)))
9 df-i3 46 . 2 (a ->3 c) = (((a' ^ c) v (a' ^ c')) v (a ^ (a' v c)))
10 df-i3 46 . 2 (b ->3 c) = (((b' ^ c) v (b' ^ c')) v (b ^ (b' v c)))
118, 9, 103tr1 63 1 (a ->3 c) = (b ->3 c)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7   ->3 wi3 14
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-i3 46
This theorem is referenced by:  2i3  254  ud3lem0b  261  bina2  283  ska14  514  i3orcom  525  i3ancom  526  bi3tr  527  i3ri3  538
  Copyright terms: Public domain W3C validator