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 706 | . 2 | |
2 | orel1 720 | . 2 | |
3 | 1, 2 | impbid2 142 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 104 wo 703 |
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 610 ax-io 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biortn 740 pm5.61 789 pm5.55dc 908 euor 2045 eueq3dc 2904 ifordc 3564 difprsnss 3718 exmidsssn 4188 opthprc 4662 frecabcl 6378 frecsuclem 6385 swoord1 6542 indpi 7304 enq0tr 7396 mulap0r 8534 mulge0 8538 leltap 8544 ap0gt0 8559 sumsplitdc 11395 coprm 12098 bdbl 13297 subctctexmid 14034 |
Copyright terms: Public domain | W3C validator |