Theorem biorf 698

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 667	. 2 |- ( ps -> ( ph \/ ps ) )
2		orel1 679	. 2 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
3	1, 2	impbid2 141	1 |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 103   \/ wo 664

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biortn  699  pm5.61  743  pm5.55dc  857  euor  1974  eueq3dc  2789  difprsnss  3575  opthprc  4489  frecabcl  6164  frecsuclem  6171  swoord1  6321  indpi  6901  enq0tr  6993  mulap0r  8092  mulge0  8096  leltap  8101  ap0gt0  8115  sumsplitdc  10826  coprm  11401