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

Theorem elimcons2 869
 Description: Consequent elimination law.
Hypotheses
Ref Expression
elimcons2.1 (a1 c) = (b1 c)
elimcons2.2 (a ∩ (c ∩ (b1 c))) ≤ (b ∪ (c ∪ (a1 c) ))
Assertion
Ref Expression
elimcons2 ab

Proof of Theorem elimcons2
StepHypRef Expression
1 elimcons2.1 . 2 (a1 c) = (b1 c)
2 elimcons2.2 . . 3 (a ∩ (c ∩ (b1 c))) ≤ (b ∪ (c ∪ (a1 c) ))
31ax-r1 35 . . . . . . 7 (b1 c) = (a1 c)
4 df-i1 44 . . . . . . 7 (a1 c) = (a ∪ (ac))
53, 4ax-r2 36 . . . . . 6 (b1 c) = (a ∪ (ac))
65lan 77 . . . . 5 (c ∩ (b1 c)) = (c ∩ (a ∪ (ac)))
76lan 77 . . . 4 (a ∩ (c ∩ (b1 c))) = (a ∩ (c ∩ (a ∪ (ac))))
8 anass 76 . . . . 5 ((ac) ∩ (a ∪ (ac))) = (a ∩ (c ∩ (a ∪ (ac))))
98ax-r1 35 . . . 4 (a ∩ (c ∩ (a ∪ (ac)))) = ((ac) ∩ (a ∪ (ac)))
10 leor 159 . . . . 5 (ac) ≤ (a ∪ (ac))
1110df2le2 136 . . . 4 ((ac) ∩ (a ∪ (ac))) = (ac)
127, 9, 113tr 65 . . 3 (a ∩ (c ∩ (b1 c))) = (ac)
131ax-r4 37 . . . . . . . 8 (a1 c) = (b1 c)
14 ud1lem0c 277 . . . . . . . 8 (b1 c) = (b ∩ (bc ))
1513, 14ax-r2 36 . . . . . . 7 (a1 c) = (b ∩ (bc ))
1615lor 70 . . . . . 6 (c ∪ (a1 c) ) = (c ∪ (b ∩ (bc )))
17 ax-a2 31 . . . . . 6 (c ∪ (b ∩ (bc ))) = ((b ∩ (bc )) ∪ c )
1816, 17ax-r2 36 . . . . 5 (c ∪ (a1 c) ) = ((b ∩ (bc )) ∪ c )
1918lor 70 . . . 4 (b ∪ (c ∪ (a1 c) )) = (b ∪ ((b ∩ (bc )) ∪ c ))
20 ax-a3 32 . . . . 5 ((b ∪ (b ∩ (bc ))) ∪ c ) = (b ∪ ((b ∩ (bc )) ∪ c ))
2120ax-r1 35 . . . 4 (b ∪ ((b ∩ (bc )) ∪ c )) = ((b ∪ (b ∩ (bc ))) ∪ c )
22 ax-a2 31 . . . . . 6 (b ∪ (b ∩ (bc ))) = ((b ∩ (bc )) ∪ b)
23 lea 160 . . . . . . 7 (b ∩ (bc )) ≤ b
2423df-le2 131 . . . . . 6 ((b ∩ (bc )) ∪ b) = b
2522, 24ax-r2 36 . . . . 5 (b ∪ (b ∩ (bc ))) = b
2625ax-r5 38 . . . 4 ((b ∪ (b ∩ (bc ))) ∪ c ) = (bc )
2719, 21, 263tr 65 . . 3 (b ∪ (c ∪ (a1 c) )) = (bc )
282, 12, 27le3tr2 141 . 2 (ac) ≤ (bc )
291, 28elimcons 868 1 ab
 Colors of variables: term Syntax hints:   = wb 1   ≤ 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-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator