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

Theorem ud5lem0a 264
 Description: Introduce →5 to the left.
Hypothesis
Ref Expression
ud5lem0a.1 a = b
Assertion
Ref Expression
ud5lem0a (c5 a) = (c5 b)

Proof of Theorem ud5lem0a
StepHypRef Expression
1 ud5lem0a.1 . . . . 5 a = b
21lan 77 . . . 4 (ca) = (cb)
31lan 77 . . . 4 (ca) = (cb)
42, 32or 72 . . 3 ((ca) ∪ (ca)) = ((cb) ∪ (cb))
51ax-r4 37 . . . 4 a = b
65lan 77 . . 3 (ca ) = (cb )
74, 62or 72 . 2 (((ca) ∪ (ca)) ∪ (ca )) = (((cb) ∪ (cb)) ∪ (cb ))
8 df-i5 48 . 2 (c5 a) = (((ca) ∪ (ca)) ∪ (ca ))
9 df-i5 48 . 2 (c5 b) = (((cb) ∪ (cb)) ∪ (cb ))
107, 8, 93tr1 63 1 (c5 a) = (c5 b)
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7   →5 wi5 16 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-i5 48 This theorem is referenced by:  nom45  330  ud5  599
 Copyright terms: Public domain W3C validator