ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biorf Unicode version

Theorem biorf 744
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.)
Assertion
Ref Expression
biorf  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )

Proof of Theorem biorf
StepHypRef Expression
1 olc 711 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 725 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 143 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 105    \/ wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 615  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biortn  745  pm5.61  794  pm5.55dc  913  euor  2052  eueq3dc  2912  ifordc  3574  difprsnss  3731  exmidsssn  4203  opthprc  4678  frecabcl  6400  frecsuclem  6407  swoord1  6564  indpi  7341  enq0tr  7433  mulap0r  8572  mulge0  8576  leltap  8582  ap0gt0  8597  sumsplitdc  11440  coprm  12144  bdbl  14006  subctctexmid  14753
  Copyright terms: Public domain W3C validator