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

Theorem nomb41 299
 Description: Lemma for "Non-Orthomodular Models..." paper. (Contributed by NM, 7-Feb-1999.)
Assertion
Ref Expression
nomb41 (a4 b) = (b1 a)

Proof of Theorem nomb41
StepHypRef Expression
1 ax-a2 31 . . 3 (ab) = (ba )
2 ancom 74 . . . 4 (ab) = (ba)
32lor 70 . . 3 (b ∪ (ab)) = (b ∪ (ba))
41, 32an 79 . 2 ((ab) ∩ (b ∪ (ab))) = ((ba ) ∩ (b ∪ (ba)))
5 df-id4 53 . 2 (a4 b) = ((ab) ∩ (b ∪ (ab)))
6 df-id1 50 . 2 (b1 a) = ((ba ) ∩ (b ∪ (ba)))
74, 5, 63tr1 63 1 (a4 b) = (b1 a)
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7   ≡1 wid1 18   ≡4 wid4 21 This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40  df-id1 50  df-id4 53 This theorem is referenced by:  nomcon3  304  nomcon4  305  nom31  320  nom34  323  nom61  338  nom64  341
 Copyright terms: Public domain W3C validator