Theorem biorf 733

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 700	. 2 |- ( ps -> ( ph \/ ps ) )
2		orel1 714	. 2 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
3	1, 2	impbid2 142	1 |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   \/ wo 697

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 604  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biortn  734  pm5.61  783  pm5.55dc  898  euor  2023  eueq3dc  2853  difprsnss  3653  exmidsssn  4120  opthprc  4585  frecabcl  6289  frecsuclem  6296  swoord1  6451  indpi  7143  enq0tr  7235  mulap0r  8370  mulge0  8374  leltap  8380  ap0gt0  8395  sumsplitdc  11194  coprm  11811  bdbl  12661  subctctexmid  13185