Theorem biorf 751

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 718	. 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
2		orel1 732	. 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))
3	1, 2	impbid2 143	1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))

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

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 620  ax-io 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  752  pm5.61  801  pm5.55dc  920  3bior1fd  1388  3bior2fd  1390  euor  2105  eueq3dc  2980  ifordc  3647  difprsnss  3811  exmidsssn  4292  opthprc  4777  frecabcl  6565  frecsuclem  6572  swoord1  6731  indpi  7562  enq0tr  7654  mulap0r  8795  mulge0  8799  leltap  8805  ap0gt0  8820  sumsplitdc  11998  coprm  12721  gsumval2  13485  bdbl  15233  eupth2lem1  16315  eupth2lem2dc  16316  eupth2lem3lem6fi  16328  subctctexmid  16627