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

Theorem biorf 716
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 683 . 2 (𝜓 → (𝜑𝜓))
2 orel1 697 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 142 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 104  wo 680
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 587  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biortn  717  pm5.61  766  pm5.55dc  881  euor  2001  eueq3dc  2829  difprsnss  3626  exmidsssn  4093  opthprc  4558  frecabcl  6262  frecsuclem  6269  swoord1  6424  indpi  7114  enq0tr  7206  mulap0r  8340  mulge0  8344  leltap  8350  ap0gt0  8364  sumsplitdc  11141  coprm  11718  bdbl  12567  subctctexmid  12998
  Copyright terms: Public domain W3C validator