Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  biorf GIF version

Theorem biorf 734
 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
StepHypRef Expression
1 olc 701 . 2 (𝜓 → (𝜑𝜓))
2 orel1 715 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 142 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   ∨ wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  biortn  735  pm5.61  784  pm5.55dc  899  euor  2032  eueq3dc  2886  difprsnss  3694  exmidsssn  4162  opthprc  4634  frecabcl  6340  frecsuclem  6347  swoord1  6502  indpi  7245  enq0tr  7337  mulap0r  8473  mulge0  8477  leltap  8483  ap0gt0  8498  sumsplitdc  11311  coprm  11998  bdbl  12863  subctctexmid  13533
 Copyright terms: Public domain W3C validator