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

Theorem biorf 739
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 706 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 720 . 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 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