Theorem biorf 395

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 374	. 2 |- ( ps -> ( ph \/ ps ) )
2		orel1 372	. 2 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
3	1, 2	impbid2 196	1 |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358

This theorem is referenced by:  biortn  396  pm5.61  694  pm5.55  868  3bior1fd  1289  3bior2fd  1291  cadan  1398  euor  2281  eueq3  3069  unineq  3551  ifor  3739  difprsnss  3894  disjprg  4168  disjxun  4170  opthwiener  4418  opthprc  4884  swoord1  6893  brwdomn0  7493  fpwwe2lem13  8473  ne0gt0  9134  xrinfmss  10844  sumsplit  12507  sadadd2lem2  12917  coprm  13055  vdwlem11  13314  lvecvscan  16138  lvecvscan2  16139  mplcoe1  16483  mplcoe2  16485  xrsxmet  18793  itg2split  19594  plydiveu  20168  quotcan  20179  coseq1  20383  angrtmuld  20603  leibpilem2  20734  leibpi  20735  wilthlem2  20805  nb3graprlem2  21414  eupath2lem2  21653  eupath2lem3  21654  nmlnogt0  22251  hvmulcan  22527  hvmulcan2  22528  xrdifh  24096  axcontlem7  25813  itgaddnclem2  26163  pr1eqbg  27944  elpadd0  30291

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-or 360