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

Theorem wfh4 426
 Description: Weak structural analog of Foulis-Holland Theorem.
Hypotheses
Ref Expression
wfh.1 C (a, b) = 1
wfh.2 C (a, c) = 1
Assertion
Ref Expression
wfh4 ((b ∪ (ac)) ≡ ((ba) ∩ (bc))) = 1

Proof of Theorem wfh4
StepHypRef Expression
1 wfh.1 . . . . 5 C (a, b) = 1
21wcomcom4 417 . . . 4 C (a , b ) = 1
3 wfh.2 . . . . 5 C (a, c) = 1
43wcomcom4 417 . . . 4 C (a , c ) = 1
52, 4wfh2 424 . . 3 ((b ∩ (ac )) ≡ ((ba ) ∪ (bc ))) = 1
6 anor2 89 . . . . 5 (b ∩ (ac )) = (b ∪ (ac ) )
76bi1 118 . . . 4 ((b ∩ (ac )) ≡ (b ∪ (ac ) ) ) = 1
8 df-a 40 . . . . . . . 8 (ac) = (ac )
98bi1 118 . . . . . . 7 ((ac) ≡ (ac ) ) = 1
109wr1 197 . . . . . 6 ((ac ) ≡ (ac)) = 1
1110wlor 368 . . . . 5 ((b ∪ (ac ) ) ≡ (b ∪ (ac))) = 1
1211wr4 199 . . . 4 ((b ∪ (ac ) ) ≡ (b ∪ (ac)) ) = 1
137, 12wr2 371 . . 3 ((b ∩ (ac )) ≡ (b ∪ (ac)) ) = 1
14 oran 87 . . . . 5 ((ba ) ∪ (bc )) = ((ba ) ∩ (bc ) )
1514bi1 118 . . . 4 (((ba ) ∪ (bc )) ≡ ((ba ) ∩ (bc ) ) ) = 1
16 oran 87 . . . . . . . 8 (ba) = (ba )
1716bi1 118 . . . . . . 7 ((ba) ≡ (ba ) ) = 1
18 oran 87 . . . . . . . 8 (bc) = (bc )
1918bi1 118 . . . . . . 7 ((bc) ≡ (bc ) ) = 1
2017, 19w2an 373 . . . . . 6 (((ba) ∩ (bc)) ≡ ((ba ) ∩ (bc ) )) = 1
2120wr1 197 . . . . 5 (((ba ) ∩ (bc ) ) ≡ ((ba) ∩ (bc))) = 1
2221wr4 199 . . . 4 (((ba ) ∩ (bc ) ) ≡ ((ba) ∩ (bc)) ) = 1
2315, 22wr2 371 . . 3 (((ba ) ∪ (bc )) ≡ ((ba) ∩ (bc)) ) = 1
245, 13, 23w3tr2 375 . 2 ((b ∪ (ac)) ≡ ((ba) ∩ (bc)) ) = 1
2524wcon1 207 1 ((b ∪ (ac)) ≡ ((ba) ∩ (bc))) = 1
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8   C wcmtr 29 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-wom 361 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134 This theorem is referenced by:  ska2  432  ska4  433  woml6  436
 Copyright terms: Public domain W3C validator