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

Theorem wlan 370
 Description: Weak orthomodular law.
Hypothesis
Ref Expression
wlan.1 (ab) = 1
Assertion
Ref Expression
wlan ((ca) ≡ (cb)) = 1

Proof of Theorem wlan
StepHypRef Expression
1 ancom 74 . . 3 (ca) = (ac)
2 ancom 74 . . 3 (cb) = (bc)
31, 22bi 99 . 2 ((ca) ≡ (cb)) = ((ac) ≡ (bc))
4 wlan.1 . . 3 (ab) = 1
54wran 369 . 2 ((ac) ≡ (bc)) = 1
63, 5ax-r2 36 1 ((ca) ≡ (cb)) = 1
 Colors of variables: term Syntax hints:   = wb 1   ≡ tb 5   ∩ wa 7  1wt 8 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-le1 130  df-le2 131 This theorem is referenced by:  w2an  373  wleoa  376  wom4  380  wcomlem  382  wletr  396  wlbtr  398  wcbtr  411  wcomcom2  415  wcom3ii  419  wfh1  423  wfh2  424  wlem14  430  wdid0id1  1110  wdid0id3  1112  wdid0id4  1113
 Copyright terms: Public domain W3C validator