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

Theorem biorf 696
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 665 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 677 . 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 662
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 578  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biortn  697  pm5.61  741  pm5.55dc  853  euor  1968  eueq3dc  2767  difprsnss  3526  opthprc  4411  frecabcl  6042  frecsuclem  6049  swoord1  6194  indpi  6583  enq0tr  6675  mulap0r  7771  mulge0  7775  leltap  7780  ap0gt0  7794  coprm  10656
  Copyright terms: Public domain W3C validator