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  2068  eueq3dc  2935  ifordc  3597  difprsnss  3757  exmidsssn  4232  opthprc  4711  frecabcl  6454  frecsuclem  6461  swoord1  6618  indpi  7404  enq0tr  7496  mulap0r  8636  mulge0  8640  leltap  8646  ap0gt0  8661  sumsplitdc  11578  coprm  12285  gsumval2  12983  bdbl  14682  subctctexmid  15561
  Copyright terms: Public domain W3C validator