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

Theorem biorf 718
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 685 . 2 (𝜓 → (𝜑𝜓))
2 orel1 699 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 142 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 104  wo 682
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 589  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biortn  719  pm5.61  768  pm5.55dc  883  euor  2003  eueq3dc  2831  difprsnss  3628  exmidsssn  4095  opthprc  4560  frecabcl  6264  frecsuclem  6271  swoord1  6426  indpi  7118  enq0tr  7210  mulap0r  8345  mulge0  8349  leltap  8355  ap0gt0  8370  sumsplitdc  11169  coprm  11749  bdbl  12599  subctctexmid  13123
  Copyright terms: Public domain W3C validator