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

Theorem biorf 696
 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 665 . 2 (𝜓 → (𝜑𝜓))
2 orel1 677 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 141 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 103   ∨ wo 662 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 578  ax-io 663 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  biortn  697  pm5.61  741  pm5.55dc  853  euor  1968  eueq3dc  2767  difprsnss  3532  opthprc  4417  frecabcl  6048  frecsuclem  6055  swoord1  6201  indpi  6594  enq0tr  6686  mulap0r  7782  mulge0  7786  leltap  7791  ap0gt0  7805  coprm  10667
 Copyright terms: Public domain W3C validator