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  705  pm5.55  885  3bior1fd  1317  3bior2fd  1319  cadanOLD  1437  euor  2305  euor2  2307  eueq3  3123  unineq  3588  ifor  3824  difprsnss  3997  disjprg  4276  disjxun  4278  opthwiener  4581  opthprc  4873  swoord1  7118  brwdomn0  7772  fpwwe2lem13  8797  ne0gt0  9467  xrinfmss  11260  sumsplit  13219  sadadd2lem2  13629  coprm  13769  vdwlem11  14035  lvecvscan  17114  lvecvscan2  17115  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  maducoeval2  18288  xrsxmet  20228  itg2split  21069  plydiveu  21649  quotcan  21660  coseq1  21869  angrtmuld  22089  leibpilem2  22221  leibpi  22222  wilthlem2  22292  tgldimor  22837  tgcolg  22867  axcontlem7  23039  nb3graprlem2  23183  eupath2lem2  23422  eupath2lem3  23423  nmlnogt0  24020  hvmulcan  24297  hvmulcan2  24298  disjunsn  25760  xrdifh  25893  itgaddnclem2  28295  pr1eqbg  29967  elpadd0  33047