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

Theorem oran2 92
Description: Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)
Assertion
Ref Expression
oran2 (ab) = (ab )

Proof of Theorem oran2
StepHypRef Expression
1 anor1 88 . . 3 (ab ) = (ab)
21ax-r1 35 . 2 (ab) = (ab )
32con3 68 1 (ab) = (ab )
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40
This theorem is referenced by:  wql2lem3  290  k1-6  353  k1-7  354  wdf-c2  384  u1lemnanb  655  u2lemnanb  656  u3lemnanb  657  u4lemnanb  658  u5lemnanb  659  u3lemnona  667  u4lemnob  673  u4lem5  764  u4lem5n  766  u2lem7n  775  bi4  840  negantlem8  856  neg3antlem2  865  mhlem2  878  marsdenlem3  882  marsdenlem4  883  oa4cl  1027
  Copyright terms: Public domain W3C validator