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

Theorem biorf 734
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 701 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 715 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 142 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
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