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  2911  ifordc  3573  difprsnss  3730  exmidsssn  4202  opthprc  4677  frecabcl  6399  frecsuclem  6406  swoord1  6563  indpi  7340  enq0tr  7432  mulap0r  8570  mulge0  8574  leltap  8580  ap0gt0  8595  sumsplitdc  11435  coprm  12138  bdbl  13896  subctctexmid  14632
  Copyright terms: Public domain W3C validator