Theorem biorf 734

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

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

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 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biortn  735  pm5.61  784  pm5.55dc  899  euor  2032  eueq3dc  2886  difprsnss  3694  exmidsssn  4163  opthprc  4636  frecabcl  6343  frecsuclem  6350  swoord1  6506  indpi  7257  enq0tr  7349  mulap0r  8485  mulge0  8489  leltap  8495  ap0gt0  8510  sumsplitdc  11324  coprm  12013  bdbl  12890  subctctexmid  13560