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  1324  3bior2fd  1326  cadanOLD  1434  euor  2308  euor2  2310  eueq3  3129  unineq  3595  ifor  3831  difprsnss  4004  disjprg  4283  disjxun  4285  opthwiener  4588  opthprc  4881  swoord1  7122  brwdomn0  7776  fpwwe2lem13  8801  ne0gt0  9471  xrinfmss  11264  sumsplit  13227  sadadd2lem2  13638  coprm  13778  vdwlem11  14044  lvecvscan  17169  lvecvscan2  17170  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  maducoeval2  18421  xrsxmet  20361  itg2split  21202  plydiveu  21739  quotcan  21750  coseq1  21959  angrtmuld  22179  leibpilem2  22311  leibpi  22312  wilthlem2  22382  tgldimor  22930  tgcolg  22962  axcontlem7  23167  nb3graprlem2  23311  eupath2lem2  23550  eupath2lem3  23551  nmlnogt0  24148  hvmulcan  24425  hvmulcan2  24426  disjunsn  25887  xrdifh  26021  itgaddnclem2  28404  pr1eqbg  30074  elpadd0  33293