Theorem biorf 406

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 385	. 2 |- ( ps -> ( ph \/ ps ) )
2		orel1 383	. 2 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
3	1, 2	impbid2 207	1 |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369

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

This theorem depends on definitions:  df-bi 188  df-or 371

This theorem is referenced by:  biortn  407  pm5.61  717  pm5.55  905  3bior1fd  1370  3bior2fd  1372  euor  2311  euor2  2313  eueq3  3245  unineq  3723  ifor  3958  difprsnss  4135  disjprg  4419  disjxun  4421  opthwiener  4722  opthprc  4901  swoord1  7404  brwdomn0  8094  fpwwe2lem13  9075  ne0gt0  9747  xrinfmss  11603  sumsplit  13829  sadadd2lem2  14424  coprm  14657  vdwlem11  14941  lvecvscan  18334  lvecvscan2  18335  mplcoe1  18689  mplcoe5  18692  maducoeval2  19664  xrsxmet  21826  itg2split  22706  plydiveu  23250  quotcan  23261  coseq1  23476  angrtmuld  23736  leibpilem2  23866  leibpi  23867  wilthlem2  23993  tgldimor  24545  tgcolg  24598  axcontlem7  24999  nb3graprlem2  25179  eupath2lem2  25705  eupath2lem3  25706  nmlnogt0  26437  hvmulcan  26724  hvmulcan2  26725  disjunsn  28207  xrdifh  28369  bj-biorfi  31172  itgaddnclem2  31966  elpadd0  33344  pr1eqbg  38858  nb3grprlem2  39244