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  892  3bior1fd  1325  3bior2fd  1327  cadanOLD  1435  euor  2319  euor2  2321  eueq3  3239  unineq  3707  ifor  3943  difprsnss  4116  disjprg  4395  disjxun  4397  opthwiener  4700  opthprc  4993  swoord1  7239  brwdomn0  7894  fpwwe2lem13  8919  ne0gt0  9589  xrinfmss  11382  sumsplit  13352  sadadd2lem2  13763  coprm  13903  vdwlem11  14169  lvecvscan  17314  lvecvscan2  17315  mplcoe1  17667  mplcoe5  17671  mplcoe2OLD  17673  maducoeval2  18577  xrsxmet  20517  itg2split  21359  plydiveu  21896  quotcan  21907  coseq1  22116  angrtmuld  22336  leibpilem2  22468  leibpi  22469  wilthlem2  22539  tgldimor  23089  tgcolg  23123  axcontlem7  23367  nb3graprlem2  23511  eupath2lem2  23750  eupath2lem3  23751  nmlnogt0  24348  hvmulcan  24625  hvmulcan2  24626  disjunsn  26086  xrdifh  26214  itgaddnclem2  28598  pr1eqbg  30268  bj-biorfi  32426  elpadd0  33776