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

Theorem wlan 370
Description: Weak orthomodular law. (Contributed by NM, 24-Sep-1997.)
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  1112  wdid0id3  1114  wdid0id4  1115
  Copyright terms: Public domain W3C validator