Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > or1r | Unicode version |
Description: Disjunction with 1. |
Ref | Expression |
---|---|
or1r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-a2 31 | . 2 | |
2 | or1 104 | . 2 | |
3 | 1, 2 | ax-r2 36 | 1 |
Colors of variables: term |
Syntax hints: wb 1 wo 6 wt 8 |
This theorem was proved from axioms: ax-a2 31 ax-a4 33 ax-r1 35 ax-r2 36 ax-r5 38 |
This theorem depends on definitions: df-t 41 |
This theorem is referenced by: ud3lem1c 568 ud3lem3 576 ud5lem1 589 i1orni1 847 lem3.3.7i1e1 1060 lem3.3.7i1e2 1061 lem3.3.7i2e1 1063 lem3.3.7i2e2 1064 |
Copyright terms: Public domain | W3C validator |