Theorem biorf 749

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 716	. 2 |- ( ps -> ( ph \/ ps ) )
2		orel1 730	. 2 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
3	1, 2	impbid2 143	1 |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   \/ wo 713

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 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  750  pm5.61  799  pm5.55dc  918  3bior1fd  1386  3bior2fd  1388  euor  2103  eueq3dc  2978  ifordc  3645  difprsnss  3807  exmidsssn  4288  opthprc  4773  frecabcl  6558  frecsuclem  6565  swoord1  6724  indpi  7550  enq0tr  7642  mulap0r  8783  mulge0  8787  leltap  8793  ap0gt0  8808  sumsplitdc  11980  coprm  12703  gsumval2  13467  bdbl  15214  subctctexmid  16511