Theorem biorf 749

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	⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))

Proof of Theorem biorf

Step	Hyp	Ref	Expression
1		olc 716	. 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
2		orel1 730	. 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))
3	1, 2	impbid2 143	1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  750  pm5.61  799  pm5.55dc  918  3bior1fd  1386  3bior2fd  1388  euor  2103  eueq3dc  2978  ifordc  3645  difprsnss  3809  exmidsssn  4290  opthprc  4775  frecabcl  6560  frecsuclem  6567  swoord1  6726  indpi  7552  enq0tr  7644  mulap0r  8785  mulge0  8789  leltap  8795  ap0gt0  8810  sumsplitdc  11983  coprm  12706  gsumval2  13470  bdbl  15217  subctctexmid  16537