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  2977  ifordc  3644  difprsnss  3806  exmidsssn  4286  opthprc  4770  frecabcl  6545  frecsuclem  6552  swoord1  6709  indpi  7529  enq0tr  7621  mulap0r  8762  mulge0  8766  leltap  8772  ap0gt0  8787  sumsplitdc  11943  coprm  12666  gsumval2  13430  bdbl  15177  subctctexmid  16366