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

Theorem ri3 253
 Description: Introduce Kalmbach implication to the right.
Hypothesis
Ref Expression
ri3.1 a = b
Assertion
Ref Expression
ri3 (a3 c) = (b3 c)

Proof of Theorem ri3
StepHypRef Expression
1 ri3.1 . . . . . 6 a = b
21ax-r4 37 . . . . 5 a = b
32ran 78 . . . 4 (ac) = (bc)
42ran 78 . . . 4 (ac ) = (bc )
53, 42or 72 . . 3 ((ac) ∪ (ac )) = ((bc) ∪ (bc ))
62ax-r5 38 . . . 4 (ac) = (bc)
71, 62an 79 . . 3 (a ∩ (ac)) = (b ∩ (bc))
85, 72or 72 . 2 (((ac) ∪ (ac )) ∪ (a ∩ (ac))) = (((bc) ∪ (bc )) ∪ (b ∩ (bc)))
9 df-i3 46 . 2 (a3 c) = (((ac) ∪ (ac )) ∪ (a ∩ (ac)))
10 df-i3 46 . 2 (b3 c) = (((bc) ∪ (bc )) ∪ (b ∩ (bc)))
118, 9, 103tr1 63 1 (a3 c) = (b3 c)
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ 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