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

Theorem biorf 698
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 667 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 679 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 141 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 103    \/ wo 664
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 580  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biortn  699  pm5.61  743  pm5.55dc  857  euor  1974  eueq3dc  2789  difprsnss  3575  opthprc  4489  frecabcl  6164  frecsuclem  6171  swoord1  6321  indpi  6901  enq0tr  6993  mulap0r  8092  mulge0  8096  leltap  8101  ap0gt0  8115  sumsplitdc  10826  coprm  11401
  Copyright terms: Public domain W3C validator