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

Theorem i1or 345
 Description: Lemma for disjunction of →1 .
Assertion
Ref Expression
i1or ((c1 a) ∪ (c1 b)) ≤ (c1 (ab))

Proof of Theorem i1or
StepHypRef Expression
1 df-i1 44 . . . 4 (c1 a) = (c ∪ (ca))
2 leo 158 . . . . . 6 a ≤ (ab)
32lelan 167 . . . . 5 (ca) ≤ (c ∩ (ab))
43lelor 166 . . . 4 (c ∪ (ca)) ≤ (c ∪ (c ∩ (ab)))
51, 4bltr 138 . . 3 (c1 a) ≤ (c ∪ (c ∩ (ab)))
6 df-i1 44 . . . 4 (c1 b) = (c ∪ (cb))
7 leor 159 . . . . . 6 b ≤ (ab)
87lelan 167 . . . . 5 (cb) ≤ (c ∩ (ab))
98lelor 166 . . . 4 (c ∪ (cb)) ≤ (c ∪ (c ∩ (ab)))
106, 9bltr 138 . . 3 (c1 b) ≤ (c ∪ (c ∩ (ab)))
115, 10lel2or 170 . 2 ((c1 a) ∪ (c1 b)) ≤ (c ∪ (c ∩ (ab)))
12 df-i1 44 . . 3 (c1 (ab)) = (c ∪ (c ∩ (ab)))
1312ax-r1 35 . 2 (c ∪ (c ∩ (ab))) = (c1 (ab))
1411, 13lbtr 139 1 ((c1 a) ∪ (c1 b)) ≤ (c1 (ab))
 Colors of variables: term Syntax hints:   ≤ wle 2  ⊥ wn 4   ∪ wo 6   ∩ wa 7   →1 wi1 12 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131 This theorem is referenced by:  orbile  843
 Copyright terms: Public domain W3C validator