ILE Home 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