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  4341  opthprc  4828  frecabcl  6675  frecsuclem  6682  swoord1  6841  indpi  7715  enq0tr  7807  mulap0r  8951  mulge0  8955  leltap  8961  ap0gt0  8976  sumsplitdc  12223  coprm  12947  gzsumval2  13772  bdbl  15746  eupth2lem1  16921  eupth2lem2dc  16922  eupth2lem3lem6fi  16934  subctctexmid  17252