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

Theorem wfh4 426
 Description: Weak structural analog of Foulis-Holland Theorem.
Hypotheses
Ref Expression
wfh.1
wfh.2
Assertion
Ref Expression
wfh4

Proof of Theorem wfh4
StepHypRef Expression
1 wfh.1 . . . . 5
21wcomcom4 417 . . . 4
3 wfh.2 . . . . 5
43wcomcom4 417 . . . 4
52, 4wfh2 424 . . 3
6 anor2 89 . . . . 5
76bi1 118 . . . 4
8 df-a 40 . . . . . . . 8
98bi1 118 . . . . . . 7
109wr1 197 . . . . . 6
1110wlor 368 . . . . 5
1211wr4 199 . . . 4
137, 12wr2 371 . . 3
14 oran 87 . . . . 5
1514bi1 118 . . . 4
16 oran 87 . . . . . . . 8
1716bi1 118 . . . . . . 7
18 oran 87 . . . . . . . 8
1918bi1 118 . . . . . . 7
2017, 19w2an 373 . . . . . 6
2120wr1 197 . . . . 5
2221wr4 199 . . . 4
2315, 22wr2 371 . . 3
245, 13, 23w3tr2 375 . 2
2524wcon1 207 1
 Colors of variables: term Syntax hints:   wb 1  wn 4   tb 5   wo 6   wa 7  wt 8   wcmtr 29 This theorem is referenced by:  ska2  432  ska4  433  woml6  436 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
 Copyright terms: Public domain W3C validator