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 701 | . 2 | |
2 | orel1 715 | . 2 | |
3 | 1, 2 | impbid2 142 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 104 wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in2 605 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biortn 735 pm5.61 784 pm5.55dc 899 euor 2032 eueq3dc 2886 difprsnss 3694 exmidsssn 4163 opthprc 4636 frecabcl 6343 frecsuclem 6350 swoord1 6506 indpi 7257 enq0tr 7349 mulap0r 8485 mulge0 8489 leltap 8495 ap0gt0 8510 sumsplitdc 11324 coprm 12013 bdbl 12890 subctctexmid 13560 |
Copyright terms: Public domain | W3C validator |