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 ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105   \/ wo 720

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used by:  biortn  757  pm5.61  806  pm5.55dc  925  3bior1fd  1393  3bior2fd  1395  euor  2112  eueq3dc  3000  ifordc  3682  difprsnss  3853  exmidsssn  4339  opthprc  4826  frecabcl  6670  frecsuclem  6677  swoord1  6836  indpi  7709  enq0tr  7801  mulap0r  8943  mulge0  8947  leltap  8953  ap0gt0  8968  sumsplitdc  12199  coprm  12922  gzsumval2  13714  bdbl  15604  eupth2lem1  16699  eupth2lem2dc  16700  eupth2lem3lem6fi  16712  subctctexmid  17030