Theorem biorf 744

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

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

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 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  745  pm5.61  794  pm5.55dc  913  euor  2052  eueq3dc  2911  ifordc  3573  difprsnss  3730  exmidsssn  4202  opthprc  4677  frecabcl  6399  frecsuclem  6406  swoord1  6563  indpi  7340  enq0tr  7432  mulap0r  8570  mulge0  8574  leltap  8580  ap0gt0  8595  sumsplitdc  11435  coprm  12138  bdbl  13896  subctctexmid  14632