Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biorf | Unicode version |
Description: A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.) |
Ref | Expression |
---|---|
biorf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | olc 664 | . 2 | |
2 | orel1 676 | . 2 | |
3 | 1, 2 | impbid2 141 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 103 wo 661 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in2 577 ax-io 662 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: biortn 696 pm5.61 740 pm5.55dc 852 euor 1967 eueq3dc 2766 difprsnss 3524 opthprc 4409 frecsuclem3 6013 swoord1 6158 indpi 6532 enq0tr 6624 mulap0r 7715 mulge0 7719 leltap 7724 ap0gt0 7738 coprm 10523 |
Copyright terms: Public domain | W3C validator |