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

Theorem biorf 745
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 712 . 2 (𝜓 → (𝜑𝜓))
2 orel1 726 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 143 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 105  wo 709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biortn  746  pm5.61  795  pm5.55dc  914  euor  2064  eueq3dc  2926  ifordc  3588  difprsnss  3745  exmidsssn  4220  opthprc  4695  frecabcl  6424  frecsuclem  6431  swoord1  6588  indpi  7371  enq0tr  7463  mulap0r  8602  mulge0  8606  leltap  8612  ap0gt0  8627  sumsplitdc  11472  coprm  12176  bdbl  14460  subctctexmid  15209
  Copyright terms: Public domain W3C validator