Theorem biorf 756

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

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

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 624  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  757  pm5.61  806  pm5.55dc  925  3bior1fd  1393  3bior2fd  1395  euor  2112  eueq3dc  3000  ifordc  3679  difprsnss  3848  exmidsssn  4334  opthprc  4821  frecabcl  6660  frecsuclem  6667  swoord1  6826  indpi  7699  enq0tr  7791  mulap0r  8933  mulge0  8937  leltap  8943  ap0gt0  8958  sumsplitdc  12177  coprm  12900  gzsumval2  13691  bdbl  15527  eupth2lem1  16613  eupth2lem2dc  16614  eupth2lem3lem6fi  16626  subctctexmid  16944