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

Step	Hyp	Ref	Expression
1		olc 665	. 2 |- ( ps -> ( ph \/ ps ) )
2		orel1 677	. 2 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
3	1, 2	impbid2 141	1 |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )

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