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

Theorem orbi 842
 Description: Disjunction of biconditionals. (Contributed by NM, 5-Jul-2000.)
Assertion
Ref Expression
orbi ((ac) ∪ (bc)) = (((a2 c) ∪ (b2 c)) ∩ ((c1 a) ∪ (c1 b)))

Proof of Theorem orbi
StepHypRef Expression
1 dfb 94 . . 3 (ac) = ((ac) ∪ (ac ))
2 dfb 94 . . 3 (bc) = ((bc) ∪ (bc ))
31, 22or 72 . 2 ((ac) ∪ (bc)) = (((ac) ∪ (ac )) ∪ ((bc) ∪ (bc )))
4 ax-a2 31 . 2 (((ac) ∪ (ac )) ∪ ((bc) ∪ (bc ))) = (((bc) ∪ (bc )) ∪ ((ac) ∪ (ac )))
5 ax-a3 32 . . 3 (((bc) ∪ (bc )) ∪ ((ac) ∪ (ac ))) = ((bc) ∪ ((bc ) ∪ ((ac) ∪ (ac ))))
6 ancom 74 . . . . . . . 8 (ac) = (ca)
76lor 70 . . . . . . 7 ((bc ) ∪ (ac)) = ((bc ) ∪ (ca))
8 imp3 841 . . . . . . . 8 ((b2 c) ∩ (c1 a)) = ((bc ) ∪ (ca))
98ax-r1 35 . . . . . . 7 ((bc ) ∪ (ca)) = ((b2 c) ∩ (c1 a))
107, 9ax-r2 36 . . . . . 6 ((bc ) ∪ (ac)) = ((b2 c) ∩ (c1 a))
1110ax-r5 38 . . . . 5 (((bc ) ∪ (ac)) ∪ (ac )) = (((b2 c) ∩ (c1 a)) ∪ (ac ))
12 ax-a3 32 . . . . 5 (((bc ) ∪ (ac)) ∪ (ac )) = ((bc ) ∪ ((ac) ∪ (ac )))
13 df-i1 44 . . . . . . . 8 (c1 a) = (c ∪ (ca))
14 lear 161 . . . . . . . . . . 11 (ac ) ≤ c
15 leo 158 . . . . . . . . . . 11 c ≤ (c ∪ (ca))
1614, 15letr 137 . . . . . . . . . 10 (ac ) ≤ (c ∪ (ca))
1716lecom 180 . . . . . . . . 9 (ac ) C (c ∪ (ca))
1817comcom 453 . . . . . . . 8 (c ∪ (ca)) C (ac )
1913, 18bctr 181 . . . . . . 7 (c1 a) C (ac )
20 comi12 707 . . . . . . 7 (c1 a) C (b2 c)
2119, 20fh4rc 482 . . . . . 6 (((b2 c) ∩ (c1 a)) ∪ (ac )) = (((b2 c) ∪ (ac )) ∩ ((c1 a) ∪ (ac )))
2213ax-r5 38 . . . . . . . 8 ((c1 a) ∪ (ac )) = ((c ∪ (ca)) ∪ (ac ))
23 ax-a2 31 . . . . . . . 8 ((c ∪ (ca)) ∪ (ac )) = ((ac ) ∪ (c ∪ (ca)))
2416df-le2 131 . . . . . . . 8 ((ac ) ∪ (c ∪ (ca))) = (c ∪ (ca))
2522, 23, 243tr 65 . . . . . . 7 ((c1 a) ∪ (ac )) = (c ∪ (ca))
2625lan 77 . . . . . 6 (((b2 c) ∪ (ac )) ∩ ((c1 a) ∪ (ac ))) = (((b2 c) ∪ (ac )) ∩ (c ∪ (ca)))
2721, 26ax-r2 36 . . . . 5 (((b2 c) ∩ (c1 a)) ∪ (ac )) = (((b2 c) ∪ (ac )) ∩ (c ∪ (ca)))
2811, 12, 273tr2 64 . . . 4 ((bc ) ∪ ((ac) ∪ (ac ))) = (((b2 c) ∪ (ac )) ∩ (c ∪ (ca)))
2928lor 70 . . 3 ((bc) ∪ ((bc ) ∪ ((ac) ∪ (ac )))) = ((bc) ∪ (((b2 c) ∪ (ac )) ∩ (c ∪ (ca))))
30 df-i2 45 . . . . . . . 8 (b2 c) = (c ∪ (bc ))
3130ax-r5 38 . . . . . . 7 ((b2 c) ∪ (ac )) = ((c ∪ (bc )) ∪ (ac ))
32 ax-a3 32 . . . . . . 7 ((c ∪ (bc )) ∪ (ac )) = (c ∪ ((bc ) ∪ (ac )))
3331, 32ax-r2 36 . . . . . 6 ((b2 c) ∪ (ac )) = (c ∪ ((bc ) ∪ (ac )))
34 lear 161 . . . . . . . . 9 (bc) ≤ c
35 leo 158 . . . . . . . . 9 c ≤ (c ∪ ((bc ) ∪ (ac )))
3634, 35letr 137 . . . . . . . 8 (bc) ≤ (c ∪ ((bc ) ∪ (ac )))
3736lecom 180 . . . . . . 7 (bc) C (c ∪ ((bc ) ∪ (ac )))
3837comcom 453 . . . . . 6 (c ∪ ((bc ) ∪ (ac ))) C (bc)
3933, 38bctr 181 . . . . 5 ((b2 c) ∪ (ac )) C (bc)
40 lea 160 . . . . . . . . . . 11 (c ∩ (ca) ) ≤ c
4140, 35letr 137 . . . . . . . . . 10 (c ∩ (ca) ) ≤ (c ∪ ((bc ) ∪ (ac )))
4241lecom 180 . . . . . . . . 9 (c ∩ (ca) ) C (c ∪ ((bc ) ∪ (ac )))
4342comcom 453 . . . . . . . 8 (c ∪ ((bc ) ∪ (ac ))) C (c ∩ (ca) )
44 anor1 88 . . . . . . . 8 (c ∩ (ca) ) = (c ∪ (ca))
4543, 44cbtr 182 . . . . . . 7 (c ∪ ((bc ) ∪ (ac ))) C (c ∪ (ca))
4645comcom7 460 . . . . . 6 (c ∪ ((bc ) ∪ (ac ))) C (c ∪ (ca))
4733, 46bctr 181 . . . . 5 ((b2 c) ∪ (ac )) C (c ∪ (ca))
4839, 47fh4 472 . . . 4 ((bc) ∪ (((b2 c) ∪ (ac )) ∩ (c ∪ (ca)))) = (((bc) ∪ ((b2 c) ∪ (ac ))) ∩ ((bc) ∪ (c ∪ (ca))))
4930lor 70 . . . . . . . 8 ((bc) ∪ (b2 c)) = ((bc) ∪ (c ∪ (bc )))
50 leo 158 . . . . . . . . . 10 c ≤ (c ∪ (bc ))
5134, 50letr 137 . . . . . . . . 9 (bc) ≤ (c ∪ (bc ))
5251df-le2 131 . . . . . . . 8 ((bc) ∪ (c ∪ (bc ))) = (c ∪ (bc ))
5349, 52ax-r2 36 . . . . . . 7 ((bc) ∪ (b2 c)) = (c ∪ (bc ))
5453ax-r5 38 . . . . . 6 (((bc) ∪ (b2 c)) ∪ (ac )) = ((c ∪ (bc )) ∪ (ac ))
55 ax-a3 32 . . . . . 6 (((bc) ∪ (b2 c)) ∪ (ac )) = ((bc) ∪ ((b2 c) ∪ (ac )))
56 ax-a2 31 . . . . . . . 8 ((c ∪ (bc )) ∪ (c ∪ (ac ))) = ((c ∪ (ac )) ∪ (c ∪ (bc )))
57 orordi 112 . . . . . . . 8 (c ∪ ((bc ) ∪ (ac ))) = ((c ∪ (bc )) ∪ (c ∪ (ac )))
58 df-i2 45 . . . . . . . . 9 (a2 c) = (c ∪ (ac ))
5958, 302or 72 . . . . . . . 8 ((a2 c) ∪ (b2 c)) = ((c ∪ (ac )) ∪ (c ∪ (bc )))
6056, 57, 593tr1 63 . . . . . . 7 (c ∪ ((bc ) ∪ (ac ))) = ((a2 c) ∪ (b2 c))
6132, 60ax-r2 36 . . . . . 6 ((c ∪ (bc )) ∪ (ac )) = ((a2 c) ∪ (b2 c))
6254, 55, 613tr2 64 . . . . 5 ((bc) ∪ ((b2 c) ∪ (ac ))) = ((a2 c) ∪ (b2 c))
63 or12 80 . . . . . 6 ((bc) ∪ (c ∪ (ca))) = (c ∪ ((bc) ∪ (ca)))
64 ax-a2 31 . . . . . . 7 ((c ∪ (bc)) ∪ (c ∪ (ca))) = ((c ∪ (ca)) ∪ (c ∪ (bc)))
65 orordi 112 . . . . . . 7 (c ∪ ((bc) ∪ (ca))) = ((c ∪ (bc)) ∪ (c ∪ (ca)))
66 df-i1 44 . . . . . . . . 9 (c1 b) = (c ∪ (cb))
67 ancom 74 . . . . . . . . . 10 (cb) = (bc)
6867lor 70 . . . . . . . . 9 (c ∪ (cb)) = (c ∪ (bc))
6966, 68ax-r2 36 . . . . . . . 8 (c1 b) = (c ∪ (bc))
7013, 692or 72 . . . . . . 7 ((c1 a) ∪ (c1 b)) = ((c ∪ (ca)) ∪ (c ∪ (bc)))
7164, 65, 703tr1 63 . . . . . 6 (c ∪ ((bc) ∪ (ca))) = ((c1 a) ∪ (c1 b))
7263, 71ax-r2 36 . . . . 5 ((bc) ∪ (c ∪ (ca))) = ((c1 a) ∪ (c1 b))
7362, 722an 79 . . . 4 (((bc) ∪ ((b2 c) ∪ (ac ))) ∩ ((bc) ∪ (c ∪ (ca)))) = (((a2 c) ∪ (b2 c)) ∩ ((c1 a) ∪ (c1 b)))
7448, 73ax-r2 36 . . 3 ((bc) ∪ (((b2 c) ∪ (ac )) ∩ (c ∪ (ca)))) = (((a2 c) ∪ (b2 c)) ∩ ((c1 a) ∪ (c1 b)))
755, 29, 743tr 65 . 2 (((bc) ∪ (bc )) ∪ ((ac) ∪ (ac ))) = (((a2 c) ∪ (b2 c)) ∩ ((c1 a) ∪ (c1 b)))
763, 4, 753tr 65 1 ((ac) ∪ (bc)) = (((a2 c) ∪ (b2 c)) ∩ ((c1 a) ∪ (c1 b)))
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7   →1 wi1 12   →2 wi2 13 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-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by:  orbile  843
 Copyright terms: Public domain W3C validator