Theorem biorf 405

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 384	. 2 |- ( ps -> ( ph \/ ps ) )
2		orel1 382	. 2 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )
3	1, 2	impbid2 204	1 |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368

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 185  df-or 370

This theorem is referenced by:  biortn  406  pm5.61  712  pm5.55  895  3bior1fd  1334  3bior2fd  1336  cadanOLD  1444  euor  2332  euor2  2334  eueq3  3278  unineq  3748  ifor  3986  difprsnss  4162  disjprg  4443  disjxun  4445  opthwiener  4749  opthprc  5046  swoord1  7337  brwdomn0  7991  fpwwe2lem13  9016  ne0gt0  9685  xrinfmss  11497  sumsplit  13542  sadadd2lem2  13955  coprm  14096  vdwlem11  14364  lvecvscan  17540  lvecvscan2  17541  mplcoe1  17898  mplcoe5  17902  mplcoe2OLD  17904  maducoeval2  18909  xrsxmet  21049  itg2split  21891  plydiveu  22428  quotcan  22439  coseq1  22648  angrtmuld  22868  leibpilem2  23000  leibpi  23001  wilthlem2  23071  tgldimor  23621  tgcolg  23669  axcontlem7  23949  nb3graprlem2  24128  eupath2lem2  24654  eupath2lem3  24655  nmlnogt0  25388  hvmulcan  25665  hvmulcan2  25666  disjunsn  27126  xrdifh  27259  itgaddnclem2  29651  pr1eqbg  31764  bj-biorfi  33253  elpadd0  34605