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

Theorem biorf 698
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 667 . 2 (𝜓 → (𝜑𝜓))
2 orel1 679 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 141 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103  wo 664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biortn  699  pm5.61  743  pm5.55dc  857  euor  1974  eueq3dc  2787  difprsnss  3570  opthprc  4477  frecabcl  6146  frecsuclem  6153  swoord1  6301  indpi  6880  enq0tr  6972  mulap0r  8068  mulge0  8072  leltap  8077  ap0gt0  8091  sumsplitdc  10789  coprm  11216
  Copyright terms: Public domain W3C validator