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

Theorem wfh3 425
 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
wfh3 ((a ∪ (bc)) ≡ ((ab) ∩ (ac))) = 1

Proof of Theorem wfh3
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, 4wfh1 423 . . 3 ((a ∩ (bc )) ≡ ((ab ) ∪ (ac ))) = 1
6 anor2 89 . . . . 5 (a ∩ (bc )) = (a ∪ (bc ) )
76bi1 118 . . . 4 ((a ∩ (bc )) ≡ (a ∪ (bc ) ) ) = 1
8 df-a 40 . . . . . . . 8 (bc) = (bc )
98bi1 118 . . . . . . 7 ((bc) ≡ (bc ) ) = 1
109wr1 197 . . . . . 6 ((bc ) ≡ (bc)) = 1
1110wlor 368 . . . . 5 ((a ∪ (bc ) ) ≡ (a ∪ (bc))) = 1
1211wr4 199 . . . 4 ((a ∪ (bc ) ) ≡ (a ∪ (bc)) ) = 1
137, 12wr2 371 . . 3 ((a ∩ (bc )) ≡ (a ∪ (bc)) ) = 1
14 oran 87 . . . . 5 ((ab ) ∪ (ac )) = ((ab ) ∩ (ac ) )
1514bi1 118 . . . 4 (((ab ) ∪ (ac )) ≡ ((ab ) ∩ (ac ) ) ) = 1
16 oran 87 . . . . . . . 8 (ab) = (ab )
1716bi1 118 . . . . . . 7 ((ab) ≡ (ab ) ) = 1
18 oran 87 . . . . . . . 8 (ac) = (ac )
1918bi1 118 . . . . . . 7 ((ac) ≡ (ac ) ) = 1
2017, 19w2an 373 . . . . . 6 (((ab) ∩ (ac)) ≡ ((ab ) ∩ (ac ) )) = 1
2120wr1 197 . . . . 5 (((ab ) ∩ (ac ) ) ≡ ((ab) ∩ (ac))) = 1
2221wr4 199 . . . 4 (((ab ) ∩ (ac ) ) ≡ ((ab) ∩ (ac)) ) = 1
2315, 22wr2 371 . . 3 (((ab ) ∪ (ac )) ≡ ((ab) ∩ (ac)) ) = 1
245, 13, 23w3tr2 375 . 2 ((a ∪ (bc)) ≡ ((ab) ∩ (ac)) ) = 1
2524wcon1 207 1 ((a ∪ (bc)) ≡ ((ab) ∩ (ac))) = 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:  woml7  437  wddi3  1107
 Copyright terms: Public domain W3C validator